1  /-
  2  Copyright (c) 2019 Gabriel Ebner. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Gabriel Ebner, Sébastien Gouëzel
  5  -/
  6  import analysis.calculus.fderiv
src         └──────────────────────┘
  7  
  8  /-!
  9  
 10  # One-dimensional derivatives
 11  
 12  This file defines the derivative of a function `f : 𝕜 → F` where `𝕜` is a
 13  normed field and `F` is a normed space over this field. The derivative of
 14  such a function `f` at a point `x` is given by an element `f' : F`.
 15  
 16  The theory is developed analogously to the [Fréchet
 17  derivatives](./fderiv.lean). We first introduce predicates defined in terms
 18  of the corresponding predicates for Fréchet derivatives:
 19  
 20   - `has_deriv_at_filter f f' x L` states that the function `f` has the
 21      derivative `f'` at the point `x` as `x` goes along the filter `L`.
 22  
 23   - `has_deriv_within_at f f' s x` states that the function `f` has the
 24      derivative `f'` at the point `x` within the subset `s`.
 25  
 26   - `has_deriv_at f f' x` states that the function `f` has the derivative `f'`
 27      at the point `x`.
 28  
 29  For the last two notions we also define a functional version:
 30  
 31    - `deriv_within f s x` is a derivative of `f` at `x` within `s`. If the
 32      derivative does not exist, then `deriv_within f s x` equals zero.
 33  
 34    - `deriv f x` is a derivative of `f` at `x`. If the derivative does not
 35      exist, then `deriv f x` equals zero.
 36  
 37  The theorems `fderiv_within_deriv_within` and `fderiv_deriv` show that the
 38  one-dimensional derivatives coincide with the general Fréchet derivatives.
 39  
 40  We also show the existence and compute the derivatives of:
 41    - constants
 42    - the identity function
 43    - linear maps
 44    - addition
 45    - negation
 46    - subtraction
 47    - multiplication
 48    - inverse `x → x⁻¹`
 49    - multiplication of two functions in `𝕜 → 𝕜`
 50    - multiplication of a function in `𝕜 → 𝕜` and of a function in `𝕜 → E`
 51    - composition of a function in `𝕜 → F` with a function in `𝕜 → 𝕜`
 52    - composition of a function in `F → E` with a function in `𝕜 → F`
 53    - division
 54    - polynomials
 55  
 56  For most binary operations we also define `const_op` and `op_const` theorems for the cases when
 57  the first or second argument is a constant. This makes writing chains of `has_deriv_at`'s easier,
 58  and they more frequently lead to the desired result.
 59  
 60  ## Implementation notes
 61  
 62  Most of the theorems are direct restatements of the corresponding theorems
 63  for Fréchet derivatives.
 64  
 65  -/
 66  
 67  universes u v w
 68  noncomputable theory
 69  open_locale classical topological_space
 70  open filter asymptotics set
 71  open continuous_linear_map (smul_right smul_right_one_eq_iff)
 72  
 73  set_option class.instance_max_depth 100
doc             └──────────────────────┘
 74  
 75  variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
id                           └──────────────────────┘
src                          └──────────────────────┘
typ                          └──────────────────────┘
doc                          └──────────────────────┘
 76  
 77  section
 78  variables {F : Type v} [normed_group F] [normed_space 𝕜 F]
id                           └──────────┘     └──────────┘
src                          └──────────┘     └──────────┘
typ                          └──────────┘     └──────────┘
doc                          └──────────┘     └──────────┘
 79  variables {E : Type w} [normed_group E] [normed_space 𝕜 E]
id                           └──────────┘     └──────────┘
src                          └──────────┘     └──────────┘
typ                          └──────────┘     └──────────┘
doc                          └──────────┘     └──────────┘
 80  
 81  /--
 82  `f` has the derivative `f'` at the point `x` as `x` goes along the filter `L`.
 83  
 84  That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges along the filter `L`.
 85  -/
 86  def has_deriv_at_filter (f : 𝕜 → F) (f' : F) (x : 𝕜) (L : filter 𝕜) :=
id                                                         └────┘ 
src                                                            └────┘
typ                                                        └────┘ 
 87  has_fderiv_at_filter f (smul_right 1 f' : 𝕜 →L[𝕜] F) x L
id   └──────────────────┘   └────────┘   └┘    └─┘    
src  └──────────────────┘    └────────┘          └─┘ 
typ  └──────────────────┘   └────────┘   └┘    └─┘    
doc  └──────────────────┘    └────────┘          └─┘ 
 88  
 89  /--
 90  `f` has the derivative `f'` at the point `x` within the subset `s`.
 91  
 92  That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x` inside `s`.
 93  -/
 94  def has_deriv_within_at (f : 𝕜 → F) (f' : F) (s : set 𝕜) (x : 𝕜) :=
id                                                  └─┘        
src                                                    └─┘
typ                                                 └─┘        
 95  has_deriv_at_filter f f' x (nhds_within x s)
id   └─────────────────┘  └┘   └─────────┘  
src  └─────────────────┘         └─────────┘
typ  └─────────────────┘  └┘   └─────────┘  
doc  └─────────────────┘         └─────────┘
 96  
 97  /--
 98  `f` has the derivative `f'` at the point `x`.
 99  
100  That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x`.
101  -/
102  def has_deriv_at (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
id                                           
typ                                          
103  has_deriv_at_filter f f' x (𝓝 x)
id   └─────────────────┘  └┘    
src  └─────────────────┘         
typ  └─────────────────┘  └┘    
doc  └─────────────────┘         
104  
105  /--
106  Derivative of `f` at the point `x` within the set `s`, if it exists.  Zero otherwise.
107  
108  If the derivative exists (i.e., `∃ f', has_deriv_within_at f f' s x`), then
109  `f x' = f x + (x' - x) • deriv_within f s x + o(x' - x)` where `x'` converges to `x` inside `s`.
110  -/
111  def deriv_within (f : 𝕜 → F) (s : set 𝕜) (x : 𝕜) :=
id                                   └─┘        
src                                    └─┘
typ                                  └─┘        
112  (fderiv_within 𝕜 f s x : 𝕜 →L[𝕜] F) 1
id    └───────────┘        └─┘ 
src   └───────────┘             └─┘ 
typ   └───────────┘        └─┘ 
doc   └───────────┘             └─┘ 
113  
114  /--
115  Derivative of `f` at the point `x`, if it exists.  Zero otherwise.
116  
117  If the derivative exists (i.e., `∃ f', has_deriv_at f f' x`), then
118  `f x' = f x + (x' - x) • deriv f x + o(x' - x)` where `x'` converges to `x`.
119  -/
120  def deriv (f : 𝕜 → F) (x : 𝕜) :=
id                            
typ                           
121  (fderiv 𝕜 f x : 𝕜 →L[𝕜] F) 1
id    └────┘       └─┘ 
src   └────┘           └─┘ 
typ   └────┘       └─┘ 
doc   └────┘           └─┘ 
122  
123  variables {f f₀ f₁ g : 𝕜 → F}
124  variables {f' f₀' f₁' g' : F}
125  variables {x : 𝕜}
126  variables {s t : set 𝕜}
id                    └─┘
src                   └─┘
typ                   └─┘
127  variables {L L₁ L₂ : filter 𝕜}
id                        └────┘
src                       └────┘
typ                       └────┘
128  
129  /-- Expressing `has_fderiv_at_filter f f' x L` in terms of `has_deriv_at_filter` -/
130  lemma has_fderiv_at_filter_iff_has_deriv_at_filter {f' : 𝕜 →L[𝕜] F} :
id                                                             └─┘ 
src                                                             └─┘ 
typ                                                            └─┘ 
doc                                                             └─┘ 
131    has_fderiv_at_filter f f' x L ↔ has_deriv_at_filter f (f' 1) x L :=
id     └──────────────────┘  └┘    └─────────────────┘   └┘     
src    └──────────────────┘           └─────────────────┘
typ    └──────────────────┘  └┘    └─────────────────┘   └┘     
doc    └──────────────────┘            └─────────────────┘
132  by simp [has_deriv_at_filter]
id            └─────────────────┘
src     └────┘└─────────────────┘└─
typ     └────┘└─────────────────┘└─
doc     └────┘└─────────────────┘└─
txt     └────┘                   └─
par     └────┘                   └─
pid                            
st     └───────────────────────────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  /-- Expressing `has_fderiv_within_at f f' s x` in terms of `has_deriv_within_at` -/
135  lemma has_fderiv_within_at_iff_has_deriv_within_at {f' : 𝕜 →L[𝕜] F} :
id                                                             └─┘ 
src                                                             └─┘ 
typ                                                            └─┘ 
doc                                                             └─┘ 
136    has_fderiv_within_at f f' s x ↔ has_deriv_within_at f (f' 1) s x :=
id     └──────────────────┘  └┘    └─────────────────┘   └┘     
src    └──────────────────┘           └─────────────────┘
typ    └──────────────────┘  └┘    └─────────────────┘   └┘     
doc    └──────────────────┘            └─────────────────┘
137  by simp [has_deriv_within_at, has_deriv_at_filter, has_fderiv_within_at]
id            └─────────────────┘  └─────────────────┘  └──────────────────┘
src     └────┘└─────────────────┘└┘└─────────────────┘└┘└──────────────────┘└─
typ     └────┘└─────────────────┘└┘└─────────────────┘└┘└──────────────────┘└─
doc     └────┘└─────────────────┘└┘└─────────────────┘└┘└──────────────────┘└─
txt     └────┘                   └┘                   └┘                    └─
par     └────┘                   └┘                   └┘                    └─
pid                            └┘                   └┘                    
st     └──────────────────────────────────────────────────────────────────────
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139  /-- Expressing `has_deriv_within_at f f' s x` in terms of `has_fderiv_within_at` -/
140  lemma has_deriv_within_at_iff_has_fderiv_within_at {f' : F} :
id                                                            
typ                                                           
141    has_deriv_within_at f f' s x ↔
id     └─────────────────┘  └┘   
src    └─────────────────┘          
typ    └─────────────────┘  └┘   
doc    └─────────────────┘
142    has_fderiv_within_at f (smul_right 1 f' : 𝕜 →L[𝕜] F) s x :=
id     └──────────────────┘   └────────┘   └┘    └─┘    
src    └──────────────────┘    └────────┘          └─┘ 
typ    └──────────────────┘   └────────┘   └┘    └─┘    
doc    └──────────────────┘    └────────┘          └─┘ 
143  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
144  
145  /-- Expressing `has_fderiv_at f f' x` in terms of `has_deriv_at` -/
146  lemma has_fderiv_at_iff_has_deriv_at {f' : 𝕜 →L[𝕜] F} :
id                                               └─┘ 
src                                               └─┘ 
typ                                              └─┘ 
doc                                               └─┘ 
147    has_fderiv_at f f' x ↔ has_deriv_at f (f' 1) x :=
id     └───────────┘  └┘   └──────────┘   └┘    
src    └───────────┘         └──────────┘
typ    └───────────┘  └┘   └──────────┘   └┘    
doc    └───────────┘          └──────────┘
148  by simp [has_deriv_at, has_deriv_at_filter, has_fderiv_at]
id            └──────────┘  └─────────────────┘  └───────────┘
src     └────┘└──────────┘└┘└─────────────────┘└┘└───────────┘└─
typ     └────┘└──────────┘└┘└─────────────────┘└┘└───────────┘└─
doc     └────┘└──────────┘└┘└─────────────────┘└┘└───────────┘└─
txt     └────┘            └┘                   └┘             └─
par     └────┘            └┘                   └┘             └─
pid                     └┘                   └┘             
st     └────────────────────────────────────────────────────────
149  
src  
typ  
doc  
txt  
par  
pid  
st   
150  /-- Expressing `has_deriv_at f f' x` in terms of `has_fderiv_at` -/
151  lemma has_deriv_at_iff_has_fderiv_at {f' : F} :
id                                              
typ                                             
152    has_deriv_at f f' x ↔
id     └──────────┘  └┘  
src    └──────────┘        
typ    └──────────┘  └┘  
doc    └──────────┘
153    has_fderiv_at f (smul_right 1 f' : 𝕜 →L[𝕜] F) x :=
id     └───────────┘   └────────┘   └┘    └─┘   
src    └───────────┘    └────────┘          └─┘ 
typ    └───────────┘   └────────┘   └┘    └─┘   
doc    └───────────┘    └────────┘          └─┘ 
154  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
155  
156  lemma deriv_within_zero_of_not_differentiable_within_at
157    (h : ¬ differentiable_within_at 𝕜 f s x) : deriv_within f s x = 0 :=
id           └──────────────────────┘        └──────────┘    
src          └──────────────────────┘            └──────────┘       
typ          └──────────────────────┘        └──────────┘    
doc           └──────────────────────┘            └──────────┘
158  by { unfold deriv_within, rw fderiv_within_zero_of_not_differentiable_within_at, simp, assumption }
id                                └────────────────────────────────────────────────┘
src       └─────────────────┘  └─┘└────────────────────────────────────────────────┘  └──┘  └─────────┘
typ       └─────────────────┘  └─┘└────────────────────────────────────────────────┘  └──┘  └─────────┘
doc       └─────────────────┘  └─┘                                                    └──┘  └─────────┘
txt       └─────────────────┘  └─┘                                                    └──┘  └─────────┘
par       └─────────────────┘  └─┘                                                    └──┘  └─────────┘
pid             └───────────┘                                                                        
st     └────────────────────┘└─────────────────────────────────────────────────────┘└────┘└───────────┘└┘
159  
160  lemma deriv_zero_of_not_differentiable_at (h : ¬ differentiable_at 𝕜 f x) : deriv f x = 0 :=
id                                                   └───────────────┘       └───┘   
src                                                  └───────────────┘          └───┘     
typ                                                  └───────────────┘       └───┘   
doc                                                   └───────────────┘          └───┘
161  by { unfold deriv, rw fderiv_zero_of_not_differentiable_at, simp, assumption }
id                         └──────────────────────────────────┘
src       └──────────┘  └─┘└──────────────────────────────────┘  └──┘  └─────────┘
typ       └──────────┘  └─┘└──────────────────────────────────┘  └──┘  └─────────┘
doc       └──────────┘  └─┘                                      └──┘  └─────────┘
txt       └──────────┘  └─┘                                      └──┘  └─────────┘
par       └──────────┘  └─┘                                      └──┘  └─────────┘
pid             └────┘                                                          
st     └─────────────┘└───────────────────────────────────────┘└────┘└───────────┘└┘
162  
163  theorem unique_diff_within_at.eq_deriv (s : set 𝕜) (H : unique_diff_within_at 𝕜 s x)
id                                               └─┘        └───────────────────┘   
src                                              └─┘         └───────────────────┘
typ                                              └─┘        └───────────────────┘   
doc                                                          └───────────────────┘
164    (h : has_deriv_within_at f f' s x) (h₁ : has_deriv_within_at f f₁' s x) : f' = f₁' :=
id          └─────────────────┘  └┘          └─────────────────┘  └─┘      └┘  └─┘
src         └─────────────────┘                 └─────────────────┘                 
typ         └─────────────────┘  └┘          └─────────────────┘  └─┘      └┘  └─┘
doc         └─────────────────┘                 └─────────────────┘
165  smul_right_one_eq_iff.mp $ unique_diff_within_at.eq H h h₁
id   └───────────────────┘└─┘   └──────────────────────┘   └┘
src  └───────────────────┘└─┘   └──────────────────────┘
typ  └───────────────────┘└─┘   └──────────────────────┘   └┘
doc                             └──────────────────────┘
166  
167  theorem has_deriv_at_filter_iff_tendsto :
168    has_deriv_at_filter f f' x L ↔
id     └─────────────────┘  └┘   
src    └─────────────────┘          
typ    └─────────────────┘  └┘   
doc    └─────────────────┘
169    tendsto (λ x' : 𝕜, ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) L (𝓝 0) :=
id     └─────┘           └┘  └┘   └┘      └┘     └┘    
src    └─────┘                 └┘                             
typ    └─────┘           └┘  └┘   └┘      └┘     └┘    
doc    └─────┘                                                          
170  has_fderiv_at_filter_iff_tendsto
id   └──────────────────────────────┘
src  └──────────────────────────────┘
typ  └──────────────────────────────┘
171  
172  theorem has_deriv_within_at_iff_tendsto : has_deriv_within_at f f' s x ↔
id                                             └─────────────────┘  └┘   
src                                            └─────────────────┘          
typ                                            └─────────────────┘  └┘   
doc                                            └─────────────────┘
173    tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds_within x s) (𝓝 0) :=
id     └─────┘    └┘  └┘  └┘   └┘      └┘     └┘   └─────────┘     
src    └─────┘             └┘                           └─────────┘       
typ    └─────┘    └┘  └┘  └┘   └┘      └┘     └┘   └─────────┘     
doc    └─────┘                                                    └─────────┘       
174  has_fderiv_at_filter_iff_tendsto
id   └──────────────────────────────┘
src  └──────────────────────────────┘
typ  └──────────────────────────────┘
175  
176  theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔
id                                      └──────────┘  └┘  
src                                     └──────────┘        
typ                                     └──────────┘  └┘  
doc                                     └──────────┘
177    tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝 x) (𝓝 0) :=
id     └─────┘    └┘  └┘  └┘   └┘      └┘     └┘       
src    └─────┘             └┘                                
typ    └─────┘    └┘  └┘  └┘   └┘      └┘     └┘       
doc    └─────┘                                                         
178  has_fderiv_at_filter_iff_tendsto
id   └──────────────────────────────┘
src  └──────────────────────────────┘
typ  └──────────────────────────────┘
179  
180  /-- If the domain has dimension one, then Fréchet derivative is equivalent to the classical
181  definition with a limit. In this version we have to take the limit along the subset `-{x}`,
182  because for `y=x` the slope equals zero due to the convention `0⁻¹=0`. -/
183  lemma has_deriv_at_filter_iff_tendsto_slope {x : 𝕜} {L : filter 𝕜} :
id                                                           └────┘ 
src                                                           └────┘
typ                                                          └────┘ 
184    has_deriv_at_filter f f' x L ↔
id     └─────────────────┘  └┘   
src    └─────────────────┘          
typ    └─────────────────┘  └┘   
doc    └─────────────────┘
185      tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (L ⊓ principal (-{x})) (𝓝 f') :=
id       └─────┘          └┘             └───────┘        └┘
src      └─────┘             └┘                  └───────┘        
typ      └─────┘          └┘             └───────┘        └┘
doc      └─────┘                                     └───────┘          
186  begin
st   └─────
187    conv_lhs { simp only [has_deriv_at_filter_iff_tendsto, (normed_field.norm_inv _).symm,
id                           └─────────────────────────────┘   └───────────────────┘
src    └─────────┘└─────────┘└─────────────────────────────┘└┘ └───────────────────┘└─────────
typ    └─────────┘└─────────┘└─────────────────────────────┘└┘ └───────────────────┘└─────────
txt    └─────────┘└─────────┘                               └┘                      └─────────
par    └─────────┘└─────────┘                               └┘                      └─────────
pid            └───────────┘                               └┘                      └─────────
st   ───────────┘└────────────────────────────────────────────────────────────────────────────
188      (norm_smul _ _).symm, tendsto_zero_iff_norm_tendsto_zero.symm] },
id        └───────┘
src  ───┘ └───────┘└──────────┘                                       └┘
typ  ───┘ └───────┘└──────────┘└─────────────────────────────────────┘└┘
txt  ───┘          └──────────┘                                       └┘
par  ───┘          └──────────┘                                       └┘
pid  ───┘          └──────────┘                                       └─┘
st   ──────────────────────────────────────────────────────────────────┘└┘
189    conv_rhs { rw [← nhds_translation f', tendsto_comap_iff] },
id                      └──────────────┘ └┘  └───────────────┘
src    └─────────┘└────┘└──────────────┘  └┘└───────────────┘└┘
typ    └─────────┘└────┘└──────────────┘└┘└┘└───────────────┘└┘
txt    └─────────┘└────┘                  └┘                 └┘
par    └─────────┘└────┘                  └┘                 └┘
pid            └──────┘                  └┘                 └─┘
st   ───────────┘└────────────────────────┘└─────────────────┘ └┘
190    refine (tendsto_inf_principal_nhds_iff_of_forall_eq $ by simp).symm.trans (tendsto_congr' _),
id             └─────────────────────────────────────────┘                        └────────────┘
src    └─────┘ └─────────────────────────────────────────┘   └──┘└───────────┘ └────────────┘└─┘
typ    └─────┘ └─────────────────────────────────────────┘   └──┘└───────────┘ └────────────┘└─┘
doc    └─────┘ └─────────────────────────────────────────┘   └──┘└───────────┘               └─┘
txt    └─────┘                                               └──┘└───────────┘               └─┘
par    └─────┘                                               └──┘└───────────┘               └─┘
pid                                                         └────────────────┘               └─┘
st   ─────────────────────────────────────────────────────────┘└───┘└─────────────────────────────┘└─
191    rw mem_inf_principal,
id        └───────────────┘
src    └─┘└───────────────┘
typ    └─┘└───────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────┘└─
192    refine univ_mem_sets' (λ z hz, _),
id            └────────────┘
src    └─────┘└────────────┘  └───────┘
typ    └─────┘└────────────┘  └───────┘
doc    └─────┘                └───────┘
txt    └─────┘                └───────┘
par    └─────┘                └───────┘
pid                          └───────┘
st   ──────────────────────────────────┘└─
193    have : z ≠ x, by simpa [function.comp] using hz,
id                          └───────────┘        └┘
src    └─────┘       └─────┘└───────────┘└──────┘
typ    └─────┘     └─────┘└───────────┘└──────┘└┘
doc    └─────┘        └─────┘             └──────┘
txt    └─────┘        └─────┘             └──────┘
par    └─────┘        └─────┘             └──────┘
pid    └───┘└┘                          └────┘
st   ─────────────┘                                   └─
194    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
195    rw [smul_sub, ← mul_smul, inv_mul_cancel (sub_ne_zero.2 this), one_smul]
id         └──────┘    └──────┘  └────────────┘  └─────────┘   └──┘   └──────┘
src    └──┘└──────┘└──┘└──────┘└┘└────────────┘ └─────────┘└─┘    └─┘└──────┘└┘
typ    └──┘└──────┘└──┘└──────┘└┘└────────────┘ └─────────┘└─┘└──┘└─┘└──────┘└┘
doc    └──┘        └──┘        └┘                          └─┘    └─┘        └┘
txt    └──┘        └──┘        └┘                          └─┘    └─┘        └┘
par    └──┘        └──┘        └┘                          └─┘    └─┘        └┘
pid      └┘        └──┘        └┘                          └─┘    └─┘        
st   ─────────────┘└──────────┘└───────────────────────────────────┘└────────┘
196  end
st   └─┘
197  
198  lemma has_deriv_within_at_iff_tendsto_slope {x : 𝕜} {s : set 𝕜} :
id                                                           └─┘ 
src                                                           └─┘
typ                                                          └─┘ 
199    has_deriv_within_at f f' s x ↔
id     └─────────────────┘  └┘   
src    └─────────────────┘          
typ    └─────────────────┘  └┘   
doc    └─────────────────┘
200      tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (s \ {x})) (𝓝 f') :=
id       └─────┘          └┘           └─────────┘           └┘
src      └─────┘             └┘               └─────────┘             
typ      └─────┘          └┘           └─────────┘           └┘
doc      └─────┘                                 └─────────┘               
201  begin
st   └─────
202    simp only [has_deriv_within_at, nhds_within, diff_eq, lattice.inf_assoc.symm, inf_principal.symm],
id                └─────────────────┘  └─────────┘  └─────┘
src    └─────────┘└─────────────────┘└┘└─────────┘└┘└─────┘└┘                      └┘                  
typ    └─────────┘└─────────────────┘└┘└─────────┘└┘└─────┘└┘└────────────────────┘└┘└────────────────┘
doc    └─────────┘└─────────────────┘└┘└─────────┘└┘       └┘                      └┘                  
txt    └─────────┘                   └┘           └┘       └┘                      └┘                  
par    └─────────┘                   └┘           └┘       └┘                      └┘                  
pid        └──┘└┘                   └┘           └┘       └┘                      └┘                  
st   ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─
203    exact has_deriv_at_filter_iff_tendsto_slope
id           └───────────────────────────────────┘
src    └────┘└───────────────────────────────────┘
typ    └────┘└───────────────────────────────────┘
doc    └────┘└───────────────────────────────────┘
txt    └────┘                                     
par    └────┘                                     
pid                                              
st   ─────────────────────────────────────────────┘
204  end
st   └─┘
205  
206  lemma has_deriv_within_at_iff_tendsto_slope' {x : 𝕜} {s : set 𝕜} (hs : x ∉ s) :
id                                                            └─┘           
src                                                            └─┘            
typ                                                           └─┘           
207    has_deriv_within_at f f' s x ↔
id     └─────────────────┘  └┘   
src    └─────────────────┘          
typ    └─────────────────┘  └┘   
doc    └─────────────────┘
208      tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x s) (𝓝 f') :=
id       └─────┘          └┘           └─────────┘      └┘
src      └─────┘             └┘               └─────────┘       
typ      └─────┘          └┘           └─────────┘      └┘
doc      └─────┘                                 └─────────┘       
209  begin
st   └─────
210    convert ← has_deriv_within_at_iff_tendsto_slope,
id               └───────────────────────────────────┘
src    └────────┘└───────────────────────────────────┘
typ    └────────┘└───────────────────────────────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid           └┘
st   ────────────────────────────────────────────────┘└─
211    exact diff_singleton_eq_self hs
id           └────────────────────┘ └┘
src    └────┘└────────────────────┘  
typ    └────┘└────────────────────┘└┘
doc    └────┘                        
txt    └────┘                        
par    └────┘                        
pid                                 
st   ─────────────────────────────────┘
212  end
st   └─┘
213  
214  lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} :
id                                             
typ                                            
215    has_deriv_at f f' x ↔
id     └──────────┘  └┘  
src    └──────────┘        
typ    └──────────┘  └┘  
doc    └──────────┘
216      tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (-{x})) (𝓝 f') :=
id       └─────┘          └┘           └─────────┘         └┘
src      └─────┘             └┘               └─────────┘          
typ      └─────┘          └┘           └─────────┘         └┘
doc      └─────┘                                 └─────────┘            
217  has_deriv_at_filter_iff_tendsto_slope
id   └───────────────────────────────────┘
src  └───────────────────────────────────┘
typ  └───────────────────────────────────┘
doc  └───────────────────────────────────┘
218  
219  theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔
id                                             └──────────┘  └┘  
src                                            └──────────┘        
typ                                            └──────────┘  └┘  
doc                                            └──────────┘
220    is_o (λh, f (x + h) - f x - h • f') (λh, h) (𝓝 0) :=
id     └──┘                 └┘         
src    └──┘                                     
typ    └──┘                 └┘         
doc    └──┘                                         
221  has_fderiv_at_iff_is_o_nhds_zero
id   └──────────────────────────────┘
src  └──────────────────────────────┘
typ  └──────────────────────────────┘
222  
223  theorem has_deriv_at_filter.mono (h : has_deriv_at_filter f f' x L₂) (hst : L₁ ≤ L₂) :
id                                         └─────────────────┘  └┘  └┘         └┘  └┘
src                                        └─────────────────┘                      
typ                                        └─────────────────┘  └┘  └┘         └┘  └┘
doc                                        └─────────────────┘
224    has_deriv_at_filter f f' x L₁ :=
id     └─────────────────┘  └┘  └┘
src    └─────────────────┘
typ    └─────────────────┘  └┘  └┘
doc    └─────────────────┘
225  has_fderiv_at_filter.mono h hst
id   └───────────────────────┘  └─┘
src  └───────────────────────┘
typ  └───────────────────────┘  └─┘
226  
227  theorem has_deriv_within_at.mono (h : has_deriv_within_at f f' t x) (hst : s ⊆ t) :
id                                         └─────────────────┘  └┘             
src                                        └─────────────────┘                    
typ                                        └─────────────────┘  └┘             
doc                                        └─────────────────┘
228    has_deriv_within_at f f' s x :=
id     └─────────────────┘  └┘  
src    └─────────────────┘
typ    └─────────────────┘  └┘  
doc    └─────────────────┘
229  has_fderiv_within_at.mono h hst
id   └───────────────────────┘  └─┘
src  └───────────────────────┘
typ  └───────────────────────┘  └─┘
230  
231  theorem has_deriv_at.has_deriv_at_filter (h : has_deriv_at f f' x) (hL : L ≤ 𝓝 x) :
id                                                 └──────────┘  └┘            
src                                                └──────────┘                  
typ                                                └──────────┘  └┘            
doc                                                └──────────┘                   
232    has_deriv_at_filter f f' x L :=
id     └─────────────────┘  └┘  
src    └─────────────────┘
typ    └─────────────────┘  └┘  
doc    └─────────────────┘
233  has_fderiv_at.has_fderiv_at_filter h hL
id   └────────────────────────────────┘  └┘
src  └────────────────────────────────┘
typ  └────────────────────────────────┘  └┘
234  
235  theorem has_deriv_at.has_deriv_within_at
236    (h : has_deriv_at f f' x) : has_deriv_within_at f f' s x :=
id          └──────────┘  └┘     └─────────────────┘  └┘  
src         └──────────┘           └─────────────────┘
typ         └──────────┘  └┘     └─────────────────┘  └┘  
doc         └──────────┘           └─────────────────┘
237  has_fderiv_at.has_fderiv_within_at h
id   └────────────────────────────────┘ 
src  └────────────────────────────────┘
typ  └────────────────────────────────┘ 
238  
239  lemma has_deriv_within_at.differentiable_within_at (h : has_deriv_within_at f f' s x) :
id                                                           └─────────────────┘  └┘  
src                                                          └─────────────────┘
typ                                                          └─────────────────┘  └┘  
doc                                                          └─────────────────┘
240    differentiable_within_at 𝕜 f s x :=
id     └──────────────────────┘    
src    └──────────────────────┘
typ    └──────────────────────┘    
doc    └──────────────────────┘
241  has_fderiv_within_at.differentiable_within_at h
id   └───────────────────────────────────────────┘ 
src  └───────────────────────────────────────────┘
typ  └───────────────────────────────────────────┘ 
242  
243  lemma has_deriv_at.differentiable_at (h : has_deriv_at f f' x) : differentiable_at 𝕜 f x :=
id                                             └──────────┘  └┘     └───────────────┘   
src                                            └──────────┘           └───────────────┘
typ                                            └──────────┘  └┘     └───────────────┘   
doc                                            └──────────┘           └───────────────┘
244  has_fderiv_at.differentiable_at h
id   └─────────────────────────────┘ 
src  └─────────────────────────────┘
typ  └─────────────────────────────┘ 
245  
246  @[simp] lemma has_deriv_within_at_univ : has_deriv_within_at f f' univ x ↔ has_deriv_at f f' x :=
id                                            └─────────────────┘  └┘ └──┘   └──────────┘  └┘ 
src                                           └─────────────────┘      └──┘    └──────────┘
typ                                           └─────────────────┘  └┘ └──┘   └──────────┘  └┘ 
doc    └──┘                                   └─────────────────┘               └──────────┘
247  has_fderiv_within_at_univ
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
248  
249  theorem has_deriv_at_unique
250    (h₀ : has_deriv_at f f₀' x) (h₁ : has_deriv_at f f₁' x) : f₀' = f₁' :=
id           └──────────┘  └─┘         └──────────┘  └─┘     └─┘  └─┘
src          └──────────┘                └──────────┘                
typ          └──────────┘  └─┘         └──────────┘  └─┘     └─┘  └─┘
doc          └──────────┘                └──────────┘
251  smul_right_one_eq_iff.mp $ has_fderiv_at_unique h₀ h₁
id   └───────────────────┘└─┘   └──────────────────┘ └┘ └┘
src  └───────────────────┘└─┘   └──────────────────┘
typ  └───────────────────┘└─┘   └──────────────────┘ └┘ └┘
252  
253  lemma has_deriv_within_at_inter' (h : t ∈ nhds_within x s) :
id                                           └─────────┘  
src                                           └─────────┘
typ                                          └─────────┘  
doc                                            └─────────┘
254    has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x :=
id     └─────────────────┘  └┘        └─────────────────┘  └┘  
src    └─────────────────┘                └─────────────────┘
typ    └─────────────────┘  └┘        └─────────────────┘  └┘  
doc    └─────────────────┘                  └─────────────────┘
255  has_fderiv_within_at_inter' h
id   └─────────────────────────┘ 
src  └─────────────────────────┘
typ  └─────────────────────────┘ 
256  
257  lemma has_deriv_within_at_inter (h : t ∈ 𝓝 x) :
id                                           
src                                          
typ                                          
doc                                           
258    has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x :=
id     └─────────────────┘  └┘        └─────────────────┘  └┘  
src    └─────────────────┘                └─────────────────┘
typ    └─────────────────┘  └┘        └─────────────────┘  └┘  
doc    └─────────────────┘                  └─────────────────┘
259  has_fderiv_within_at_inter h
id   └────────────────────────┘ 
src  └────────────────────────┘
typ  └────────────────────────┘ 
260  
261  lemma has_deriv_within_at.union (hs : has_deriv_within_at f f' s x) (ht : has_deriv_within_at f f' t x) :
id                                         └─────────────────┘  └┘          └─────────────────┘  └┘  
src                                        └─────────────────┘                 └─────────────────┘
typ                                        └─────────────────┘  └┘          └─────────────────┘  └┘  
doc                                        └─────────────────┘                 └─────────────────┘
262    has_deriv_within_at f f' (s ∪ t) x :=
id     └─────────────────┘  └┘      
src    └─────────────────┘         
typ    └─────────────────┘  └┘      
doc    └─────────────────┘
263  begin
st   └─────
264    simp only [has_deriv_within_at, nhds_within_union],
id                └─────────────────┘  └───────────────┘
src    └─────────┘└─────────────────┘└┘└───────────────┘
typ    └─────────┘└─────────────────┘└┘└───────────────┘
doc    └─────────┘└─────────────────┘└┘                 
txt    └─────────┘                   └┘                 
par    └─────────┘                   └┘                 
pid        └──┘└┘                   └┘                 
st   ───────────────────────────────────────────────────┘└─
265    exact hs.join ht,
id           └─────┘ └┘
src    └────┘└─────┘
typ    └────┘└─────┘└┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid                
st   ─────────────────┘└─
266  end
st   ──┘
267  
268  lemma has_deriv_within_at.nhds_within (h : has_deriv_within_at f f' s x)
id                                              └─────────────────┘  └┘  
src                                             └─────────────────┘
typ                                             └─────────────────┘  └┘  
doc                                             └─────────────────┘
269    (ht : s ∈ nhds_within x t) : has_deriv_within_at f f' t x :=
id             └─────────┘      └─────────────────┘  └┘  
src             └─────────┘        └─────────────────┘
typ            └─────────┘      └─────────────────┘  └┘  
doc              └─────────┘        └─────────────────┘
270  (has_deriv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _))
id    └────────────────────────┘ └┘    └───┘  └────────────────┘
src   └────────────────────────┘        └───┘  └────────────────┘
typ   └────────────────────────┘ └┘    └───┘  └────────────────┘
271  
272  lemma has_deriv_within_at.has_deriv_at (h : has_deriv_within_at f f' s x) (hs : s ∈ 𝓝 x) :
id                                               └─────────────────┘  └┘             
src                                              └─────────────────┘                    
typ                                              └─────────────────┘  └┘             
doc                                              └─────────────────┘                     
273    has_deriv_at f f' x :=
id     └──────────┘  └┘ 
src    └──────────┘
typ    └──────────┘  └┘ 
doc    └──────────┘
274  has_fderiv_within_at.has_fderiv_at h hs
id   └────────────────────────────────┘  └┘
src  └────────────────────────────────┘
typ  └────────────────────────────────┘  └┘
275  
276  lemma differentiable_within_at.has_deriv_within_at (h : differentiable_within_at 𝕜 f s x) :
id                                                           └──────────────────────┘    
src                                                          └──────────────────────┘
typ                                                          └──────────────────────┘    
doc                                                          └──────────────────────┘
277    has_deriv_within_at f (deriv_within f s x) s x :=
id     └─────────────────┘   └──────────┘      
src    └─────────────────┘    └──────────┘
typ    └─────────────────┘   └──────────┘      
doc    └─────────────────┘    └──────────┘
278  show has_fderiv_within_at _ _ _ _, by { convert h.has_fderiv_within_at, simp [deriv_within] }
id        └──────────────────┘                       └────────────────────┘        └──────────┘
src       └──────────────────┘               └──────┘└────────────────────┘  └────┘└──────────┘└┘
typ       └──────────────────┘               └──────┘└────────────────────┘  └────┘└──────────┘└┘
doc       └──────────────────┘               └──────┘                        └────┘└──────────┘└┘
txt                                          └──────┘                        └────┘            └┘
par                                          └──────┘                        └────┘            └┘
pid                                                                                         
st                                        └───────────────────────────────┘└────────────────────┘└┘
279  
280  lemma differentiable_at.has_deriv_at (h : differentiable_at 𝕜 f x) : has_deriv_at f (deriv f x) x :=
id                                             └───────────────┘       └──────────┘   └───┘    
src                                            └───────────────┘          └──────────┘    └───┘
typ                                            └───────────────┘       └──────────┘   └───┘    
doc                                            └───────────────┘          └──────────┘    └───┘
281  show has_fderiv_at _ _ _, by { convert h.has_fderiv_at, simp [deriv] }
id        └───────────┘                     └─────────────┘        └───┘
src       └───────────┘             └──────┘└─────────────┘  └────┘└───┘└┘
typ       └───────────┘             └──────┘└─────────────┘  └────┘└───┘└┘
doc       └───────────┘             └──────┘                 └────┘└───┘└┘
txt                                 └──────┘                 └────┘     └┘
par                                 └──────┘                 └────┘     └┘
pid                                                                  
st                               └────────────────────────┘└─────────────┘└┘
282  
283  lemma has_deriv_at.deriv (h : has_deriv_at f f' x) : deriv f x = f' :=
id                                 └──────────┘  └┘     └───┘    └┘
src                                └──────────┘           └───┘     
typ                                └──────────┘  └┘     └───┘    └┘
doc                                └──────────┘           └───┘
284  has_deriv_at_unique h.differentiable_at.has_deriv_at h
id   └─────────────────┘ └────────────────┘└───────────┘ 
src  └─────────────────┘  └────────────────┘└───────────┘
typ  └─────────────────┘ └────────────────┘└───────────┘ 
285  
286  lemma has_deriv_within_at.deriv_within
287    (h : has_deriv_within_at f f' s x) (hxs : unique_diff_within_at 𝕜 s x) :
id          └─────────────────┘  └┘           └───────────────────┘   
src         └─────────────────┘                  └───────────────────┘
typ         └─────────────────┘  └┘           └───────────────────┘   
doc         └─────────────────┘                  └───────────────────┘
288    deriv_within f s x = f' :=
id     └──────────┘     └┘
src    └──────────┘       
typ    └──────────┘     └┘
doc    └──────────┘
289  hxs.eq_deriv _ h.differentiable_within_at.has_deriv_within_at h
id   └─┘└───────┘   └───────────────────────┘└──────────────────┘ 
src     └───────┘    └───────────────────────┘└──────────────────┘
typ  └─┘└───────┘   └───────────────────────┘└──────────────────┘ 
290  
291  lemma fderiv_within_deriv_within : (fderiv_within 𝕜 f s x : 𝕜 → F) 1 = deriv_within f s x :=
id                                       └───────────┘               └──────────┘   
src                                      └───────────┘                     └──────────┘
typ                                      └───────────┘               └──────────┘   
doc                                      └───────────┘                      └──────────┘
292  rfl
id   └─┘
src  └─┘
typ  └─┘
293  
294  lemma deriv_within_fderiv_within :
295    smul_right 1 (deriv_within f s x) = fderiv_within 𝕜 f s x :=
id     └────────┘    └──────────┘      └───────────┘    
src    └────────┘    └──────────┘         └───────────┘
typ    └────────┘    └──────────┘      └───────────┘    
doc    └────────┘    └──────────┘          └───────────┘
296  by simp [deriv_within]
id            └──────────┘
src     └────┘└──────────┘└─
typ     └────┘└──────────┘└─
doc     └────┘└──────────┘└─
txt     └────┘            └─
par     └────┘            └─
pid                     
st     └────────────────────
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  lemma fderiv_deriv : (fderiv 𝕜 f x : 𝕜 → F) 1 = deriv f x :=
id                         └────┘              └───┘  
src                        └────┘                   └───┘
typ                        └────┘              └───┘  
doc                        └────┘                    └───┘
299  rfl
id   └─┘
src  └─┘
typ  └─┘
300  
301  lemma deriv_fderiv :
302    smul_right 1 (deriv f x) = fderiv 𝕜 f x :=
id     └────────┘    └───┘     └────┘   
src    └────────┘    └───┘       └────┘
typ    └────────┘    └───┘     └────┘   
doc    └────────┘    └───┘        └────┘
303  by simp [deriv]
id            └───┘
src     └────┘└───┘└─
typ     └────┘└───┘└─
doc     └────┘└───┘└─
txt     └────┘     └─
par     └────┘     └─
pid              
st     └─────────────
304  
src  
typ  
doc  
txt  
par  
pid  
st   
305  lemma differentiable_at.deriv_within (h : differentiable_at 𝕜 f x)
id                                             └───────────────┘   
src                                            └───────────────┘
typ                                            └───────────────┘   
doc                                            └───────────────┘
306    (hxs : unique_diff_within_at 𝕜 s x) : deriv_within f s x = deriv f x :=
id            └───────────────────┘       └──────────┘     └───┘  
src           └───────────────────┘          └──────────┘        └───┘
typ           └───────────────────┘       └──────────┘     └───┘  
doc           └───────────────────┘          └──────────┘         └───┘
307  by { unfold deriv_within deriv, rw h.fderiv_within hxs }
id                                      └─────────────┘ └─┘
src       └───────────────────────┘  └─┘└─────────────┘   
typ       └───────────────────────┘  └─┘└─────────────┘└─┘
doc       └───────────────────────┘  └─┘                  
txt       └───────────────────────┘  └─┘                  
par       └───────────────────────┘  └─┘                  
pid             └─────────────────┘                      
st     └──────────────────────────┘└───────────────────────┘└┘
308  
309  lemma deriv_within_subset (st : s ⊆ t) (ht : unique_diff_within_at 𝕜 s x)
id                                             └───────────────────┘   
src                                              └───────────────────┘
typ                                            └───────────────────┘   
doc                                               └───────────────────┘
310    (h : differentiable_within_at 𝕜 f t x) :
id          └──────────────────────┘    
src         └──────────────────────┘
typ         └──────────────────────┘    
doc         └──────────────────────┘
311    deriv_within f s x = deriv_within f t x :=
id     └──────────┘     └──────────┘   
src    └──────────┘        └──────────┘
typ    └──────────┘     └──────────┘   
doc    └──────────┘         └──────────┘
312  ((differentiable_within_at.has_deriv_within_at h).mono st).deriv_within ht
id     └──────────────────────────────────────────┘  └──┘  └┘ └──────────┘  └┘
src    └──────────────────────────────────────────┘   └──┘     └──────────┘
typ    └──────────────────────────────────────────┘  └──┘  └┘ └──────────┘  └┘
313  
314  @[simp] lemma deriv_within_univ : deriv_within f univ = deriv f :=
id                                     └──────────┘  └──┘  └───┘ 
src                                    └──────────┘   └──┘  └───┘
typ                                    └──────────┘  └──┘  └───┘ 
doc    └──┘                            └──────────┘          └───┘
315  by { ext, unfold deriv_within deriv, rw fderiv_within_univ }
id                                           └────────────────┘
src       └─┘  └───────────────────────┘  └─┘└────────────────┘
typ       └─┘  └───────────────────────┘  └─┘└────────────────┘
doc       └─┘  └───────────────────────┘  └─┘                  
txt       └─┘  └───────────────────────┘  └─┘                  
par       └─┘  └───────────────────────┘  └─┘                  
pid                  └─────────────────┘                      
st     └────┘└─────────────────────────┘└──────────────────────┘└┘
316  
317  lemma deriv_within_inter (ht : t ∈ 𝓝 x) (hs : unique_diff_within_at 𝕜 s x) :
id                                             └───────────────────┘   
src                                              └───────────────────┘
typ                                            └───────────────────┘   
doc                                               └───────────────────┘
318    deriv_within f (s ∩ t) x = deriv_within f s x :=
id     └──────────┘         └──────────┘   
src    └──────────┘             └──────────┘
typ    └──────────┘         └──────────┘   
doc    └──────────┘               └──────────┘
319  by { unfold deriv_within, rw fderiv_within_inter ht hs }
id                                └─────────────────┘ └┘ └┘
src       └─────────────────┘  └─┘└─────────────────┘    
typ       └─────────────────┘  └─┘└─────────────────┘└┘└┘
doc       └─────────────────┘  └─┘                       
txt       └─────────────────┘  └─┘                       
par       └─────────────────┘  └─┘                       
pid             └───────────┘                           
st     └────────────────────┘└─────────────────────────────┘└┘
320  
321  section congr
322  /-! ### Congruence properties of derivatives -/
323  
324  theorem has_deriv_at_filter_congr_of_mem_sets
325    (hx : f₀ x = f₁ x) (h₀ : ∀ᶠ x in L, f₀ x = f₁ x) (h₁ : f₀' = f₁') :
id           └┘   └┘         └┘  └┘  └┘   └┘         └─┘  └─┘
src                            └┘   └┘                         
typ          └┘   └┘         └┘  └┘  └┘   └┘         └─┘  └─┘
doc                             └┘   └┘  
326    has_deriv_at_filter f₀ f₀' x L ↔ has_deriv_at_filter f₁ f₁' x L :=
id     └─────────────────┘ └┘ └─┘    └─────────────────┘ └┘ └─┘  
src    └─────────────────┘             └─────────────────┘
typ    └─────────────────┘ └┘ └─┘    └─────────────────┘ └┘ └─┘  
doc    └─────────────────┘              └─────────────────┘
327  has_fderiv_at_filter_congr_of_mem_sets hx h₀ (by simp [h₁])
id   └────────────────────────────────────┘ └┘ └┘           └┘
src  └────────────────────────────────────┘           └────┘  
typ  └────────────────────────────────────┘ └┘ └┘     └────┘└┘
doc                                                   └────┘  
txt                                                   └────┘  
par                                                   └────┘  
pid                                                         
st                                                   └────────┘
328  
329  lemma has_deriv_at_filter.congr_of_mem_sets (h : has_deriv_at_filter f f' x L)
id                                                    └─────────────────┘  └┘  
src                                                   └─────────────────┘
typ                                                   └─────────────────┘  └┘  
doc                                                   └─────────────────┘
330    (hL : ∀ᶠ x in L, f₁ x = f x) (hx : f₁ x = f x) : has_deriv_at_filter f₁ f' x L :=
id           └┘  └┘  └┘            └┘        └─────────────────┘ └┘ └┘  
src          └┘   └┘                                 └─────────────────┘
typ          └┘  └┘  └┘            └┘        └─────────────────┘ └┘ └┘  
doc          └┘   └┘                                   └─────────────────┘
331  by rwa has_deriv_at_filter_congr_of_mem_sets hx hL rfl
id          └───────────────────────────────────┘ └┘ └┘ └─┘
src     └──┘└───────────────────────────────────┘    └─┘
typ     └──┘└───────────────────────────────────┘└┘└┘└─┘
doc     └──┘                                            
txt     └──┘                                            
par     └──┘                                            
pid                                                    
st     └────────────────────────────────────────────────────
332  
src  
typ  
doc  
txt  
par  
pid  
st   
333  lemma has_deriv_within_at.congr_mono (h : has_deriv_within_at f f' s x) (ht : ∀x ∈ t, f₁ x = f x)
id                                             └─────────────────┘  └┘                └┘    
src                                            └─────────────────┘                             
typ                                            └─────────────────┘  └┘                └┘    
doc                                            └─────────────────┘
334    (hx : f₁ x = f x) (h₁ : t ⊆ s) : has_deriv_within_at f₁ f' t x :=
id           └┘                  └─────────────────┘ └┘ └┘  
src                                   └─────────────────┘
typ          └┘                  └─────────────────┘ └┘ └┘  
doc                                     └─────────────────┘
335  has_fderiv_within_at.congr_mono h ht hx h₁
id   └─────────────────────────────┘  └┘ └┘ └┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘  └┘ └┘ └┘
336  
337  lemma has_deriv_within_at.congr (h : has_deriv_within_at f f' s x) (hs : ∀x ∈ s, f₁ x = f x)
id                                        └─────────────────┘  └┘                └┘    
src                                       └─────────────────┘                              
typ                                       └─────────────────┘  └┘                └┘    
doc                                       └─────────────────┘
338    (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x :=
id           └┘        └─────────────────┘ └┘ └┘  
src                       └─────────────────┘
typ          └┘        └─────────────────┘ └┘ └┘  
doc                        └─────────────────┘
339  h.congr_mono hs hx (subset.refl _)
id   └─────────┘ └┘ └┘  └─────────┘
src   └─────────┘        └─────────┘
typ  └─────────┘ └┘ └┘  └─────────┘
340  
341  lemma has_deriv_within_at.congr_of_mem_nhds_within (h : has_deriv_within_at f f' s x)
id                                                           └─────────────────┘  └┘  
src                                                          └─────────────────┘
typ                                                          └─────────────────┘  └┘  
doc                                                          └─────────────────┘
342    (h₁ : ∀ᶠ y in nhds_within x s, f₁ y = f y) (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x :=
id           └┘  └┘ └─────────┘   └┘            └┘        └─────────────────┘ └┘ └┘  
src          └┘   └┘ └─────────┘                                   └─────────────────┘
typ          └┘  └┘ └─────────┘   └┘            └┘        └─────────────────┘ └┘ └┘  
doc          └┘   └┘ └─────────┘                                     └─────────────────┘
343  has_deriv_at_filter.congr_of_mem_sets h h₁ hx
id   └───────────────────────────────────┘  └┘ └┘
src  └───────────────────────────────────┘
typ  └───────────────────────────────────┘  └┘ └┘
344  
345  lemma has_deriv_at.congr_of_mem_nhds (h : has_deriv_at f f' x)
id                                             └──────────┘  └┘ 
src                                            └──────────┘
typ                                            └──────────┘  └┘ 
doc                                            └──────────┘
346    (h₁ : ∀ᶠ y in 𝓝 x, f₁ y = f y) : has_deriv_at f₁ f' x :=
id           └┘  └┘   └┘        └──────────┘ └┘ └┘ 
src          └┘   └┘                 └──────────┘
typ          └┘  └┘   └┘        └──────────┘ └┘ └┘ 
doc          └┘   └┘                  └──────────┘
347  has_deriv_at_filter.congr_of_mem_sets h h₁ (mem_of_nhds h₁ : _)
id   └───────────────────────────────────┘  └┘  └─────────┘ └┘
src  └───────────────────────────────────┘       └─────────┘
typ  └───────────────────────────────────┘  └┘  └─────────┘ └┘
348  
349  lemma deriv_within_congr_of_mem_nhds_within (hs : unique_diff_within_at 𝕜 s x)
id                                                     └───────────────────┘   
src                                                    └───────────────────┘
typ                                                    └───────────────────┘   
doc                                                    └───────────────────┘
350    (hL : ∀ᶠ y in nhds_within x s, f₁ y = f y) (hx : f₁ x = f x) :
id           └┘  └┘ └─────────┘   └┘            └┘    
src          └┘   └┘ └─────────┘                           
typ          └┘  └┘ └─────────┘   └┘            └┘    
doc          └┘   └┘ └─────────┘    
351    deriv_within f₁ s x = deriv_within f s x :=
id     └──────────┘ └┘    └──────────┘   
src    └──────────┘         └──────────┘
typ    └──────────┘ └┘    └──────────┘   
doc    └──────────┘          └──────────┘
352  by { unfold deriv_within, rw fderiv_within_congr_of_mem_nhds_within hs hL hx }
id                                └────────────────────────────────────┘ └┘ └┘ └┘
src       └─────────────────┘  └─┘└────────────────────────────────────┘      
typ       └─────────────────┘  └─┘└────────────────────────────────────┘└┘└┘└┘
doc       └─────────────────┘  └─┘                                            
txt       └─────────────────┘  └─┘                                            
par       └─────────────────┘  └─┘                                            
pid             └───────────┘                                                
st     └────────────────────┘└───────────────────────────────────────────────────┘└┘
353  
354  lemma deriv_within_congr (hs : unique_diff_within_at 𝕜 s x)
id                                  └───────────────────┘   
src                                 └───────────────────┘
typ                                 └───────────────────┘   
doc                                 └───────────────────┘
355    (hL : ∀y∈s, f₁ y = f y) (hx : f₁ x = f x) :
id               └┘            └┘    
src                                      
typ              └┘            └┘    
356    deriv_within f₁ s x = deriv_within f s x :=
id     └──────────┘ └┘    └──────────┘   
src    └──────────┘         └──────────┘
typ    └──────────┘ └┘    └──────────┘   
doc    └──────────┘          └──────────┘
357  by { unfold deriv_within, rw fderiv_within_congr hs hL hx }
id                                └─────────────────┘ └┘ └┘ └┘
src       └─────────────────┘  └─┘└─────────────────┘      
typ       └─────────────────┘  └─┘└─────────────────┘└┘└┘└┘
doc       └─────────────────┘  └─┘                         
txt       └─────────────────┘  └─┘                         
par       └─────────────────┘  └─┘                         
pid             └───────────┘                             
st     └────────────────────┘└────────────────────────────────┘└┘
358  
359  lemma deriv_congr_of_mem_nhds (hL : ∀ᶠ y in 𝓝 x, f₁ y = f y) : deriv f₁ x = deriv f x :=
id                                       └┘  └┘   └┘        └───┘ └┘   └───┘  
src                                      └┘   └┘                 └───┘       └───┘
typ                                      └┘  └┘   └┘        └───┘ └┘   └───┘  
doc                                      └┘   └┘                  └───┘        └───┘
360  by { unfold deriv, rwa fderiv_congr_of_mem_nhds }
id                          └──────────────────────┘
src       └──────────┘  └──┘└──────────────────────┘
typ       └──────────┘  └──┘└──────────────────────┘
doc       └──────────┘  └──┘                        
txt       └──────────┘  └──┘                        
par       └──────────┘  └──┘                        
pid             └────┘                             
st     └─────────────┘└─────────────────────────────┘└┘
361  
362  end congr
363  
364  section id
365  /-! ### Derivative of the identity -/
366  variables (s x L)
367  
368  theorem has_deriv_at_filter_id : has_deriv_at_filter id 1 x L :=
id                                    └─────────────────┘ └┘    
src                                   └─────────────────┘ └┘
typ                                   └─────────────────┘ └┘    
doc                                   └─────────────────┘
369  (is_o_zero _ _).congr_left $ by simp
id    └───────┘     └────────┘
src   └───────┘     └────────┘       └────
typ   └───────┘     └────────┘       └────
doc                                  └────
txt                                  └────
par                                  └────
pid                                      
st                                  └─────
370  
src  
typ  
doc  
txt  
par  
pid  
st   
371  theorem has_deriv_within_at_id : has_deriv_within_at id 1 s x :=
id                                    └─────────────────┘ └┘    
src                                   └─────────────────┘ └┘
typ                                   └─────────────────┘ └┘    
doc                                   └─────────────────┘
372  has_deriv_at_filter_id _ _
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
373  
374  theorem has_deriv_at_id : has_deriv_at id 1 x :=
id                             └──────────┘ └┘   
src                            └──────────┘ └┘
typ                            └──────────┘ └┘   
doc                            └──────────┘
375  has_deriv_at_filter_id _ _
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
376  
377  lemma deriv_id : deriv id x = 1 :=
id                    └───┘ └┘  
src                   └───┘ └┘   
typ                   └───┘ └┘  
doc                   └───┘
378  has_deriv_at.deriv (has_deriv_at_id x)
id   └────────────────┘  └─────────────┘ 
src  └────────────────┘  └─────────────┘
typ  └────────────────┘  └─────────────┘ 
379  
380  @[simp] lemma deriv_id' : deriv (@id 𝕜) = λ _, 1 :=
id                             └───┘   └┘      
src                            └───┘   └┘    
typ                            └───┘   └┘      
doc    └──┘                    └───┘
381  funext deriv_id
id   └────┘ └──────┘
src  └────┘ └──────┘
typ  └────┘ └──────┘
382  
383  lemma deriv_within_id (hxs : unique_diff_within_at 𝕜 s x) : deriv_within id s x = 1 :=
id                                └───────────────────┘       └──────────┘ └┘   
src                               └───────────────────┘          └──────────┘ └┘     
typ                               └───────────────────┘       └──────────┘ └┘   
doc                               └───────────────────┘          └──────────┘
384  by { unfold deriv_within, rw fderiv_within_id, simp, assumption }
id                                └──────────────┘
src       └─────────────────┘  └─┘└──────────────┘  └──┘  └─────────┘
typ       └─────────────────┘  └─┘└──────────────┘  └──┘  └─────────┘
doc       └─────────────────┘  └─┘                  └──┘  └─────────┘
txt       └─────────────────┘  └─┘                  └──┘  └─────────┘
par       └─────────────────┘  └─┘                  └──┘  └─────────┘
pid             └───────────┘                                      
st     └────────────────────┘└───────────────────┘└────┘└───────────┘└┘
385  
386  end id
387  
388  section const
389  /-! ### Derivative of constant functions -/
390  variables (c : F) (s x L)
391  
392  theorem has_deriv_at_filter_const : has_deriv_at_filter (λ x, c) 0 x L :=
id                                       └─────────────────┘           
src                                      └─────────────────┘
typ                                      └─────────────────┘           
doc                                      └─────────────────┘
393  (is_o_zero _ _).congr_left $ λ _, by simp [continuous_linear_map.zero_apply, sub_self]
id    └───────┘     └────────┘                 └──────────────────────────────┘  └──────┘
src   └───────┘     └────────┘            └────┘└──────────────────────────────┘└┘└──────┘└─
typ   └───────┘     └────────┘           └────┘└──────────────────────────────┘└┘└──────┘└─
doc                                       └────┘                                └┘        └─
txt                                       └────┘                                └┘        └─
par                                       └────┘                                └┘        └─
pid                                                                           └┘        
st                                       └──────────────────────────────────────────────────
394  
src  
typ  
doc  
txt  
par  
pid  
st   
395  theorem has_deriv_within_at_const : has_deriv_within_at (λ x, c) 0 s x :=
id                                       └─────────────────┘           
src                                      └─────────────────┘
typ                                      └─────────────────┘           
doc                                      └─────────────────┘
396  has_deriv_at_filter_const _ _ _
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
397  
398  theorem has_deriv_at_const : has_deriv_at (λ x, c) 0 x :=
id                                └──────────┘          
src                               └──────────┘
typ                               └──────────┘          
doc                               └──────────┘
399  has_deriv_at_filter_const _ _ _
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
400  
401  lemma deriv_const : deriv (λ x, c) x = 0 :=
id                       └───┘         
src                      └───┘            
typ                      └───┘         
doc                      └───┘
402  has_deriv_at.deriv (has_deriv_at_const x c)
id   └────────────────┘  └────────────────┘  
src  └────────────────┘  └────────────────┘
typ  └────────────────┘  └────────────────┘  
403  
404  @[simp] lemma deriv_const' : deriv (λ x:𝕜, c) = λ x, 0 :=
id                                └───┘             
src                               └───┘            
typ                               └───┘             
doc    └──┘                       └───┘
405  funext (λ x, deriv_const x c)
id   └────┘      └─────────┘  
src  └────┘       └─────────┘
typ  └────┘      └─────────┘  
406  
407  lemma deriv_within_const (hxs : unique_diff_within_at 𝕜 s x) : deriv_within (λ x, c) s x = 0 :=
id                                   └───────────────────┘       └──────────┘          
src                                  └───────────────────┘          └──────────┘              
typ                                  └───────────────────┘       └──────────┘          
doc                                  └───────────────────┘          └──────────┘
408  by { rw (differentiable_at_const _).deriv_within hxs, apply deriv_const }
id            └─────────────────────┘                 └─┘        └─────────┘
src       └─┘ └─────────────────────┘└───────────────┘     └────┘└─────────┘
typ       └─┘ └─────────────────────┘└───────────────┘└─┘  └────┘└─────────┘
doc       └─┘                        └───────────────┘     └────┘           
txt       └─┘                        └───────────────┘     └────┘           
par       └─┘                        └───────────────┘     └────┘           
pid                                 └───────────────┘                     
st     └────────────────────────────────────────────────┘└──────────────────┘└┘
409  
410  end const
411  
412  section is_linear_map
413  /-! ### Derivative of linear maps -/
414  variables (s x L) [is_linear_map 𝕜 f]
id                      └───────────┘
src                     └───────────┘
typ                     └───────────┘
415  
416  lemma is_linear_map.has_deriv_at_filter : has_deriv_at_filter f (f 1) x L :=
id                                             └─────────────────┘        
src                                            └─────────────────┘
typ                                            └─────────────────┘        
doc                                            └─────────────────┘
417  (is_o_zero _ _).congr_left begin
id    └───────┘     └────────┘
src   └───────┘     └────────┘
typ   └───────┘     └────────┘
st                              └─────
418    intro y,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
419    simp [add_smul],
id           └──────┘
src    └────┘└──────┘
typ    └────┘└──────┘
doc    └────┘        
txt    └────┘        
par    └────┘        
pid                
st   ────────────────┘└─
420    rw ← is_linear_map.smul f x,
id          └────────────────┘  
src    └───┘└────────────────┘ 
typ    └───┘└────────────────┘
doc    └───┘                   
txt    └───┘                   
par    └───┘                   
pid      └─┘                   
st   ────────────────────────────┘└─
421    rw ← is_linear_map.smul f y,
id          └────────────────┘  
src    └───┘└────────────────┘ 
typ    └───┘└────────────────┘
doc    └───┘                   
txt    └───┘                   
par    └───┘                   
pid      └─┘                   
st   ────────────────────────────┘└─
422    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
423  end
st   └─┘
424  
425  lemma is_linear_map.has_deriv_within_at : has_deriv_within_at f (f 1) s x :=
id                                             └─────────────────┘        
src                                            └─────────────────┘
typ                                            └─────────────────┘        
doc                                            └─────────────────┘
426  is_linear_map.has_deriv_at_filter _ _
id   └───────────────────────────────┘
src  └───────────────────────────────┘
typ  └───────────────────────────────┘
427  
428  lemma is_linear_map.has_deriv_at : has_deriv_at f (f 1) x  :=
id                                      └──────────┘       
src                                     └──────────┘
typ                                     └──────────┘       
doc                                     └──────────┘
429  is_linear_map.has_deriv_at_filter _ _
id   └───────────────────────────────┘
src  └───────────────────────────────┘
typ  └───────────────────────────────┘
430  
431  lemma is_linear_map.differentiable_at : differentiable_at 𝕜 f x :=
id                                           └───────────────┘   
src                                          └───────────────┘
typ                                          └───────────────┘   
doc                                          └───────────────┘
432  (is_linear_map.has_deriv_at _).differentiable_at
id    └────────────────────────┘   └───────────────┘
src   └────────────────────────┘   └───────────────┘
typ   └────────────────────────┘   └───────────────┘
433  
434  lemma is_linear_map.differentiable_within_at : differentiable_within_at 𝕜 f s x :=
id                                                  └──────────────────────┘    
src                                                 └──────────────────────┘
typ                                                 └──────────────────────┘    
doc                                                 └──────────────────────┘
435  (is_linear_map.differentiable_at _).differentiable_within_at
id    └─────────────────────────────┘   └──────────────────────┘
src   └─────────────────────────────┘   └──────────────────────┘
typ   └─────────────────────────────┘   └──────────────────────┘
436  
437  @[simp] lemma is_linear_map.deriv : deriv f x = f 1 :=
id                                       └───┘    
src                                      └───┘     
typ                                      └───┘    
doc    └──┘                              └───┘
438  has_deriv_at.deriv (is_linear_map.has_deriv_at _)
id   └────────────────┘  └────────────────────────┘
src  └────────────────┘  └────────────────────────┘
typ  └────────────────┘  └────────────────────────┘
439  
440  lemma is_linear_map.deriv_within (hxs : unique_diff_within_at 𝕜 s x) :
id                                           └───────────────────┘   
src                                          └───────────────────┘
typ                                          └───────────────────┘   
doc                                          └───────────────────┘
441    deriv_within f s x = f 1 :=
id     └──────────┘     
src    └──────────┘       
typ    └──────────┘     
doc    └──────────┘
442  begin
st   └─────
443    rw differentiable_at.deriv_within (is_linear_map.differentiable_at _) hxs,
id        └────────────────────────────┘  └─────────────────────────────┘    └─┘
src    └─┘└────────────────────────────┘ └─────────────────────────────┘└──┘
typ    └─┘└────────────────────────────┘ └─────────────────────────────┘└──┘└─┘
doc    └─┘                                                              └──┘
txt    └─┘                                                              └──┘
par    └─┘                                                              └──┘
pid                                                                    └──┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
444    apply is_linear_map.deriv,
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────┘└─
445    assumption
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid              
st   ────────────┘
446  end
st   └─┘
447  
448  lemma is_linear_map.differentiable : differentiable 𝕜 f :=
id                                        └────────────┘  
src                                       └────────────┘
typ                                       └────────────┘  
doc                                       └────────────┘
449  λ x, is_linear_map.differentiable_at _
id       └─────────────────────────────┘
src       └─────────────────────────────┘
typ      └─────────────────────────────┘
450  
451  lemma is_linear_map.differentiable_on : differentiable_on 𝕜 f s :=
id                                           └───────────────┘   
src                                          └───────────────┘
typ                                          └───────────────┘   
doc                                          └───────────────┘
452  is_linear_map.differentiable.differentiable_on
id   └──────────────────────────┘└────────────────┘
src  └──────────────────────────┘└────────────────┘
typ  └──────────────────────────┘└────────────────┘
453  
454  end is_linear_map
455  
456  section add
457  /-! ### Derivative of the sum of two functions -/
458  
459  theorem has_deriv_at_filter.add
460    (hf : has_deriv_at_filter f f' x L) (hg : has_deriv_at_filter g g' x L) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
461    has_deriv_at_filter (λ y, f y + g y) (f' + g') x L :=
id     └─────────────────┘             └┘  └┘   
src    └─────────────────┘                     
typ    └─────────────────┘             └┘  └┘   
doc    └─────────────────┘
462  (hf.add hg).congr_left $ by simp [add_smul, smul_add]
id    └┘└──┘ └┘ └────────┘             └──────┘  └──────┘
src     └──┘    └────────┘       └────┘└──────┘└┘└──────┘└─
typ   └┘└──┘ └┘ └────────┘       └────┘└──────┘└┘└──────┘└─
doc                              └────┘        └┘        └─
txt                              └────┘        └┘        └─
par                              └────┘        └┘        └─
pid                                          └┘        
st                              └──────────────────────────
463  
src  
typ  
doc  
txt  
par  
pid  
st   
464  theorem has_deriv_within_at.add
465    (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
466    has_deriv_within_at (λ y, f y + g y) (f' + g') s x :=
id     └─────────────────┘             └┘  └┘   
src    └─────────────────┘                     
typ    └─────────────────┘             └┘  └┘   
doc    └─────────────────┘
467  hf.add hg
id   └┘└──┘ └┘
src    └──┘
typ  └┘└──┘ └┘
468  
469  theorem has_deriv_at.add
470    (hf : has_deriv_at f f' x) (hg : has_deriv_at g g' x) :
id           └──────────┘  └┘         └──────────┘  └┘ 
src          └──────────┘               └──────────┘
typ          └──────────┘  └┘         └──────────┘  └┘ 
doc          └──────────┘               └──────────┘
471    has_deriv_at (λ x, f x + g x) (f' + g') x :=
id     └──────────┘             └┘  └┘  
src    └──────────┘                     
typ    └──────────┘             └┘  └┘  
doc    └──────────┘
472  hf.add hg
id   └┘└──┘ └┘
src    └──┘
typ  └┘└──┘ └┘
473  
474  lemma deriv_within_add (hxs : unique_diff_within_at 𝕜 s x)
id                                 └───────────────────┘   
src                                └───────────────────┘
typ                                └───────────────────┘   
doc                                └───────────────────┘
475    (hf : differentiable_within_at 𝕜 f s x) (hg : differentiable_within_at 𝕜 g s x) :
id           └──────────────────────┘            └──────────────────────┘    
src          └──────────────────────┘                └──────────────────────┘
typ          └──────────────────────┘            └──────────────────────┘    
doc          └──────────────────────┘                └──────────────────────┘
476    deriv_within (λy, f y + g y) s x = deriv_within f s x + deriv_within g s x :=
id     └──────────┘              └──────────┘     └──────────┘   
src    └──────────┘                     └──────────┘        └──────────┘
typ    └──────────┘              └──────────┘     └──────────┘   
doc    └──────────┘                       └──────────┘         └──────────┘
477  (hf.has_deriv_within_at.add hg.has_deriv_within_at).deriv_within hxs
id    └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
src     └──────────────────┘└──┘   └──────────────────┘ └──────────┘
typ   └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
478  
479  lemma deriv_add
480    (hf : differentiable_at 𝕜 f x) (hg : differentiable_at 𝕜 g x) :
id           └───────────────┘           └───────────────┘   
src          └───────────────┘              └───────────────┘
typ          └───────────────┘           └───────────────┘   
doc          └───────────────┘              └───────────────┘
481    deriv (λy, f y + g y) x = deriv f x + deriv g x :=
id     └───┘             └───┘    └───┘  
src    └───┘                   └───┘      └───┘
typ    └───┘             └───┘    └───┘  
doc    └───┘                     └───┘       └───┘
482  (hf.has_deriv_at.add hg.has_deriv_at).deriv
id    └┘└───────────┘└──┘ └┘└───────────┘ └───┘
src     └───────────┘└──┘   └───────────┘ └───┘
typ   └┘└───────────┘└──┘ └┘└───────────┘ └───┘
483  
484  theorem has_deriv_at_filter.add_const
485    (hf : has_deriv_at_filter f f' x L) (c : F) :
id           └─────────────────┘  └┘         
src          └─────────────────┘
typ          └─────────────────┘  └┘         
doc          └─────────────────┘
486    has_deriv_at_filter (λ y, f y + c) f' x L :=
id     └─────────────────┘           └┘  
src    └─────────────────┘           
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
487  add_zero f' ▸ hf.add (has_deriv_at_filter_const x L c)
id   └──────┘ └┘  └┘└──┘  └───────────────────────┘   
src  └──────┘       └──┘  └───────────────────────┘
typ  └──────┘ └┘  └┘└──┘  └───────────────────────┘   
488  
489  theorem has_deriv_within_at.add_const
490    (hf : has_deriv_within_at f f' s x) (c : F) :
id           └─────────────────┘  └┘         
src          └─────────────────┘
typ          └─────────────────┘  └┘         
doc          └─────────────────┘
491    has_deriv_within_at (λ y, f y + c) f' s x :=
id     └─────────────────┘           └┘  
src    └─────────────────┘           
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
492  hf.add_const c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
493  
494  theorem has_deriv_at.add_const
495    (hf : has_deriv_at f f' x) (c : F) :
id           └──────────┘  └┘        
src          └──────────┘
typ          └──────────┘  └┘        
doc          └──────────┘
496    has_deriv_at (λ x, f x + c) f' x :=
id     └──────────┘           └┘ 
src    └──────────┘           
typ    └──────────┘           └┘ 
doc    └──────────┘
497  hf.add_const c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
498  
499  lemma deriv_within_add_const (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
500    (hf : differentiable_within_at 𝕜 f s x) (c : F) :
id           └──────────────────────┘           
src          └──────────────────────┘
typ          └──────────────────────┘           
doc          └──────────────────────┘
501    deriv_within (λy, f y + c) s x = deriv_within f s x :=
id     └──────────┘             └──────────┘   
src    └──────────┘                   └──────────┘
typ    └──────────┘             └──────────┘   
doc    └──────────┘                     └──────────┘
502  (hf.has_deriv_within_at.add_const c).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
503  
504  lemma deriv_add_const (hf : differentiable_at 𝕜 f x) (c : F) :
id                               └───────────────┘          
src                              └───────────────┘
typ                              └───────────────┘          
doc                              └───────────────┘
505    deriv (λy, f y + c) x = deriv f x :=
id     └───┘            └───┘  
src    └───┘                 └───┘
typ    └───┘            └───┘  
doc    └───┘                   └───┘
506  (hf.has_deriv_at.add_const c).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
507  
508  theorem has_deriv_at_filter.const_add (c : F) (hf : has_deriv_at_filter f f' x L) :
id                                                      └─────────────────┘  └┘  
src                                                      └─────────────────┘
typ                                                     └─────────────────┘  └┘  
doc                                                      └─────────────────┘
509    has_deriv_at_filter (λ y, c + f y) f' x L :=
id     └─────────────────┘           └┘  
src    └─────────────────┘         
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
510  zero_add f' ▸ (has_deriv_at_filter_const x L c).add hf
id   └──────┘ └┘   └───────────────────────┘    └─┘  └┘
src  └──────┘      └───────────────────────┘       └─┘
typ  └──────┘ └┘   └───────────────────────┘    └─┘  └┘
511  
512  theorem has_deriv_within_at.const_add (c : F) (hf : has_deriv_within_at f f' s x) :
id                                                      └─────────────────┘  └┘  
src                                                      └─────────────────┘
typ                                                     └─────────────────┘  └┘  
doc                                                      └─────────────────┘
513    has_deriv_within_at (λ y, c + f y) f' s x :=
id     └─────────────────┘           └┘  
src    └─────────────────┘         
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
514  hf.const_add c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
515  
516  theorem has_deriv_at.const_add (c : F) (hf : has_deriv_at f f' x) :
id                                               └──────────┘  └┘ 
src                                               └──────────┘
typ                                              └──────────┘  └┘ 
doc                                               └──────────┘
517    has_deriv_at (λ x, c + f x) f' x :=
id     └──────────┘           └┘ 
src    └──────────┘         
typ    └──────────┘           └┘ 
doc    └──────────┘
518  hf.const_add c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
519  
520  lemma deriv_within_const_add (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
521    (c : F) (hf : differentiable_within_at 𝕜 f s x) :
id                  └──────────────────────┘    
src                  └──────────────────────┘
typ                 └──────────────────────┘    
doc                  └──────────────────────┘
522    deriv_within (λy, c + f y) s x = deriv_within f s x :=
id     └──────────┘             └──────────┘   
src    └──────────┘                   └──────────┘
typ    └──────────┘             └──────────┘   
doc    └──────────┘                     └──────────┘
523  (hf.has_deriv_within_at.const_add c).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
524  
525  lemma deriv_const_add (c : F) (hf : differentiable_at 𝕜 f x) :
id                                      └───────────────┘   
src                                      └───────────────┘
typ                                     └───────────────┘   
doc                                      └───────────────┘
526    deriv (λy, c + f y) x = deriv f x :=
id     └───┘            └───┘  
src    └───┘                 └───┘
typ    └───┘            └───┘  
doc    └───┘                   └───┘
527  (hf.has_deriv_at.const_add c).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
528  
529  end add
530  
531  section mul_vector
532  /-! ### Derivative of the multiplication of a scalar function and a vector function -/
533  variables {c : 𝕜 → 𝕜} {c' : 𝕜}
534  
535  theorem has_deriv_within_at.smul
536    (hc : has_deriv_within_at c c' s x) (hf : has_deriv_within_at f f' s x) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
537    has_deriv_within_at (λ y, c y • f y) (c x • f' + c' • f x) s x :=
id     └─────────────────┘                └┘  └┘      
src    └─────────────────┘                              
typ    └─────────────────┘                └┘  └┘      
doc    └─────────────────┘
538  begin
st   └─────
539    show has_fderiv_within_at _ _ _ _,
id          └──────────────────┘
src    └───┘└──────────────────┘└──────┘
typ    └───┘└──────────────────┘└──────┘
doc    └───┘└──────────────────┘└──────┘
txt    └───┘                    └──────┘
par    └───┘                    └──────┘
pid    └───┘                    └──────┘
st   ──────────────────────────────────┘└─
540    convert has_fderiv_within_at.smul hc hf,
id             └───────────────────────┘ └┘ └┘
src    └──────┘└───────────────────────┘  
typ    └──────┘└───────────────────────┘└┘└┘
doc    └──────┘                           
txt    └──────┘                           
par    └──────┘                           
pid                                      
st   ────────────────────────────────────────┘└─
541    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
542    simp [smul_add, (mul_smul _ _ _).symm, mul_comm]
id           └──────┘   └──────┘              └──────┘
src    └────┘└──────┘└┘ └──────┘└────────────┘└──────┘└┘
typ    └────┘└──────┘└┘ └──────┘└────────────┘└──────┘└┘
doc    └────┘        └┘         └────────────┘        └┘
txt    └────┘        └┘         └────────────┘        └┘
par    └────┘        └┘         └────────────┘        └┘
pid                └┘         └────────────┘        
st   ──────────────────────────────────────────────────┘
543  end
st   └─┘
544  
545  theorem has_deriv_at.smul
546    (hc : has_deriv_at c c' x) (hf : has_deriv_at f f' x) :
id           └──────────┘  └┘         └──────────┘  └┘ 
src          └──────────┘               └──────────┘
typ          └──────────┘  └┘         └──────────┘  └┘ 
doc          └──────────┘               └──────────┘
547    has_deriv_at (λ y, c y • f y) (c x • f' + c' • f x) x :=
id     └──────────┘                └┘  └┘     
src    └──────────┘                              
typ    └──────────┘                └┘  └┘     
doc    └──────────┘
548  begin
st   └─────
549    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
550    exact hc.smul hf
id           └─────┘ └┘
src    └────┘└─────┘  
typ    └────┘└─────┘└┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ──────────────────┘
551  end
st   └─┘
552  
553  lemma deriv_within_smul (hxs : unique_diff_within_at 𝕜 s x)
id                                  └───────────────────┘   
src                                 └───────────────────┘
typ                                 └───────────────────┘   
doc                                 └───────────────────┘
554    (hc : differentiable_within_at 𝕜 c s x) (hf : differentiable_within_at 𝕜 f s x) :
id           └──────────────────────┘            └──────────────────────┘    
src          └──────────────────────┘                └──────────────────────┘
typ          └──────────────────────┘            └──────────────────────┘    
doc          └──────────────────────┘                └──────────────────────┘
555    deriv_within (λ y, c y • f y) s x = c x • deriv_within f s x + (deriv_within c s x) • f x :=
id     └──────────┘                  └──────────┘      └──────────┘       
src    └──────────┘                           └──────────┘         └──────────┘        
typ    └──────────┘                  └──────────┘      └──────────┘       
doc    └──────────┘                              └──────────┘          └──────────┘
556  (hc.has_deriv_within_at.smul hf.has_deriv_within_at).deriv_within hxs
id    └┘└──────────────────┘└───┘ └┘└──────────────────┘ └──────────┘  └─┘
src     └──────────────────┘└───┘   └──────────────────┘ └──────────┘
typ   └┘└──────────────────┘└───┘ └┘└──────────────────┘ └──────────┘  └─┘
557  
558  lemma deriv_smul (hc : differentiable_at 𝕜 c x) (hf : differentiable_at 𝕜 f x) :
id                          └───────────────┘           └───────────────┘   
src                         └───────────────┘              └───────────────┘
typ                         └───────────────┘           └───────────────┘   
doc                         └───────────────┘              └───────────────┘
559    deriv (λ y, c y • f y) x = c x • deriv f x + (deriv c x) • f x :=
id     └───┘                 └───┘     └───┘      
src    └───┘                         └───┘       └───┘      
typ    └───┘                 └───┘     └───┘      
doc    └───┘                            └───┘        └───┘
560  (hc.has_deriv_at.smul hf.has_deriv_at).deriv
id    └┘└───────────┘└───┘ └┘└───────────┘ └───┘
src     └───────────┘└───┘   └───────────┘ └───┘
typ   └┘└───────────┘└───┘ └┘└───────────┘ └───┘
561  
562  theorem has_deriv_within_at.smul_const
563    (hc : has_deriv_within_at c c' s x) (f : F) :
id           └─────────────────┘  └┘         
src          └─────────────────┘
typ          └─────────────────┘  └┘         
doc          └─────────────────┘
564    has_deriv_within_at (λ y, c y • f) (c' • f) s x :=
id     └─────────────────┘            └┘     
src    └─────────────────┘                   
typ    └─────────────────┘            └┘     
doc    └─────────────────┘
565  begin
st   └─────
566    have := hc.smul (has_deriv_within_at_const x s f),
id             └─────┘  └───────────────────────┘   
src    └──────┘└─────┘ └───────────────────────┘   
typ    └──────┘└─────┘ └───────────────────────┘
doc    └──────┘                                    
txt    └──────┘                                    
par    └──────┘                                    
pid    └───┘└─┘                                    
st   ──────────────────────────────────────────────────┘└─
567    rwa [smul_zero, zero_add] at this
id          └───────┘  └──────┘
src    └───┘└───────┘└┘└──────┘└────────┘
typ    └───┘└───────┘└┘└──────┘└────────┘
doc    └───┘         └┘        └────────┘
txt    └───┘         └┘        └────────┘
par    └───┘         └┘        └────────┘
pid       └┘         └┘        └──────┘
st   ───────────────┘└────────┘└───────┘
568  end
st   └─┘
569  
570  theorem has_deriv_at.smul_const
571    (hc : has_deriv_at c c' x) (f : F) :
id           └──────────┘  └┘        
src          └──────────┘
typ          └──────────┘  └┘        
doc          └──────────┘
572    has_deriv_at (λ y, c y • f) (c' • f) x :=
id     └──────────┘            └┘    
src    └──────────┘                   
typ    └──────────┘            └┘    
doc    └──────────┘
573  begin
st   └─────
574    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
575    exact hc.smul_const f
id           └───────────┘ 
src    └────┘└───────────┘ 
typ    └────┘└───────────┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ───────────────────────┘
576  end
st   └─┘
577  
578  lemma deriv_within_smul_const (hxs : unique_diff_within_at 𝕜 s x)
id                                        └───────────────────┘   
src                                       └───────────────────┘
typ                                       └───────────────────┘   
doc                                       └───────────────────┘
579    (hc : differentiable_within_at 𝕜 c s x) (f : F) :
id           └──────────────────────┘           
src          └──────────────────────┘
typ          └──────────────────────┘           
doc          └──────────────────────┘
580    deriv_within (λ y, c y • f) s x = (deriv_within c s x) • f :=
id     └──────────┘               └──────────┘      
src    └──────────┘                     └──────────┘        
typ    └──────────┘               └──────────┘      
doc    └──────────┘                       └──────────┘
581  (hc.has_deriv_within_at.smul_const f).deriv_within hxs
id    └┘└──────────────────┘└─────────┘  └──────────┘  └─┘
src     └──────────────────┘└─────────┘   └──────────┘
typ   └┘└──────────────────┘└─────────┘  └──────────┘  └─┘
582  
583  lemma deriv_smul_const (hc : differentiable_at 𝕜 c x) (f : F) :
id                                └───────────────┘          
src                               └───────────────┘
typ                               └───────────────┘          
doc                               └───────────────┘
584    deriv (λ y, c y • f) x = (deriv c x) • f :=
id     └───┘              └───┘     
src    └───┘                   └───┘      
typ    └───┘              └───┘     
doc    └───┘                     └───┘
585  (hc.has_deriv_at.smul_const f).deriv
id    └┘└───────────┘└─────────┘  └───┘
src     └───────────┘└─────────┘   └───┘
typ   └┘└───────────┘└─────────┘  └───┘
586  
587  theorem has_deriv_within_at.const_smul
588    (c : 𝕜) (hf : has_deriv_within_at f f' s x) :
id                  └─────────────────┘  └┘  
src                  └─────────────────┘
typ                 └─────────────────┘  └┘  
doc                  └─────────────────┘
589    has_deriv_within_at (λ y, c • f y) (c • f') s x :=
id     └─────────────────┘              └┘   
src    └─────────────────┘                  
typ    └─────────────────┘              └┘   
doc    └─────────────────┘
590  begin
st   └─────
591    convert (has_deriv_within_at_const x s c).smul hf,
id              └───────────────────────┘          └┘
src    └──────┘ └───────────────────────┘   └─────┘
typ    └──────┘ └───────────────────────┘└─────┘└┘
doc    └──────┘                             └─────┘
txt    └──────┘                             └─────┘
par    └──────┘                             └─────┘
pid                                        └─────┘
st   ──────────────────────────────────────────────────┘└─
592    rw [zero_smul, add_zero]
id         └───────┘  └──────┘
src    └──┘└───────┘└┘└──────┘└┘
typ    └──┘└───────┘└┘└──────┘└┘
doc    └──┘         └┘        └┘
txt    └──┘         └┘        └┘
par    └──┘         └┘        └┘
pid      └┘         └┘        
st   ──────────────┘└────────┘
593  end
st   └─┘
594  
595  theorem has_deriv_at.const_smul (c : 𝕜) (hf : has_deriv_at f f' x) :
id                                                └──────────┘  └┘ 
src                                                └──────────┘
typ                                               └──────────┘  └┘ 
doc                                                └──────────┘
596    has_deriv_at (λ y, c • f y) (c • f') x :=
id     └──────────┘              └┘  
src    └──────────┘                  
typ    └──────────┘              └┘  
doc    └──────────┘
597  begin
st   └─────
598    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
599    exact hf.const_smul c
id           └───────────┘ 
src    └────┘└───────────┘ 
typ    └────┘└───────────┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ───────────────────────┘
600  end
st   └─┘
601  
602  lemma deriv_within_const_smul (hxs : unique_diff_within_at 𝕜 s x)
id                                        └───────────────────┘   
src                                       └───────────────────┘
typ                                       └───────────────────┘   
doc                                       └───────────────────┘
603    (c : 𝕜) (hf : differentiable_within_at 𝕜 f s x) :
id                  └──────────────────────┘    
src                  └──────────────────────┘
typ                 └──────────────────────┘    
doc                  └──────────────────────┘
604    deriv_within (λ y, c • f y) s x = c • deriv_within f s x :=
id     └──────────┘                └──────────┘   
src    └──────────┘                       └──────────┘
typ    └──────────┘                └──────────┘   
doc    └──────────┘                          └──────────┘
605  (hf.has_deriv_within_at.const_smul c).deriv_within hxs
id    └┘└──────────────────┘└─────────┘  └──────────┘  └─┘
src     └──────────────────┘└─────────┘   └──────────┘
typ   └┘└──────────────────┘└─────────┘  └──────────┘  └─┘
606  
607  lemma deriv_const_smul (c : 𝕜) (hf : differentiable_at 𝕜 f x) :
id                                       └───────────────┘   
src                                       └───────────────┘
typ                                      └───────────────┘   
doc                                       └───────────────┘
608    deriv (λ y, c • f y) x = c • deriv f x :=
id     └───┘               └───┘  
src    └───┘                     └───┘
typ    └───┘               └───┘  
doc    └───┘                        └───┘
609  (hf.has_deriv_at.const_smul c).deriv
id    └┘└───────────┘└─────────┘  └───┘
src     └───────────┘└─────────┘   └───┘
typ   └┘└───────────┘└─────────┘  └───┘
610  
611  end mul_vector
612  
613  section neg
614  /-! ### Derivative of the negative of a function -/
615  
616  theorem has_deriv_at_filter.neg (h : has_deriv_at_filter f f' x L) :
id                                        └─────────────────┘  └┘  
src                                       └─────────────────┘
typ                                       └─────────────────┘  └┘  
doc                                       └─────────────────┘
617    has_deriv_at_filter (λ x, -f x) (-f') x L :=
id     └─────────────────┘          └┘   
src    └─────────────────┘             
typ    └─────────────────┘          └┘   
doc    └─────────────────┘
618  h.neg.congr (by simp) (by simp)
id   └──┘└────┘
src   └──┘└────┘     └──┘      └──┘
typ  └──┘└────┘     └──┘      └──┘
doc                  └──┘      └──┘
txt                  └──┘      └──┘
par                  └──┘      └──┘
st                  └───┘     └───┘
619  
620  theorem has_deriv_within_at.neg (h : has_deriv_within_at f f' s x) :
id                                        └─────────────────┘  └┘  
src                                       └─────────────────┘
typ                                       └─────────────────┘  └┘  
doc                                       └─────────────────┘
621    has_deriv_within_at (λ x, -f x) (-f') s x :=
id     └─────────────────┘          └┘   
src    └─────────────────┘             
typ    └─────────────────┘          └┘   
doc    └─────────────────┘
622  h.neg
id   └──┘
src   └──┘
typ  └──┘
623  
624  theorem has_deriv_at.neg (h : has_deriv_at f f' x) : has_deriv_at (λ x, -f x) (-f') x :=
id                                 └──────────┘  └┘     └──────────┘          └┘  
src                                └──────────┘           └──────────┘             
typ                                └──────────┘  └┘     └──────────┘          └┘  
doc                                └──────────┘           └──────────┘
625  h.neg
id   └──┘
src   └──┘
typ  └──┘
626  
627  lemma deriv_within_neg (hxs : unique_diff_within_at 𝕜 s x)
id                                 └───────────────────┘   
src                                └───────────────────┘
typ                                └───────────────────┘   
doc                                └───────────────────┘
628    (h : differentiable_within_at 𝕜 f s x) :
id          └──────────────────────┘    
src         └──────────────────────┘
typ         └──────────────────────┘    
doc         └──────────────────────┘
629    deriv_within (λy, -f y) s x = - deriv_within f s x :=
id     └──────────┘            └──────────┘   
src    └──────────┘                 └──────────┘
typ    └──────────┘            └──────────┘   
doc    └──────────┘                    └──────────┘
630  h.has_deriv_within_at.neg.deriv_within hxs
id   └──────────────────┘└──┘└───────────┘ └─┘
src   └──────────────────┘└──┘└───────────┘
typ  └──────────────────┘└──┘└───────────┘ └─┘
631  
632  lemma deriv_neg : deriv (λy, -f y) x = - deriv f x :=
id                     └───┘           └───┘  
src                    └───┘               └───┘
typ                    └───┘           └───┘  
doc                    └───┘                  └───┘
633  if h : differentiable_at 𝕜 f x then h.has_deriv_at.neg.deriv else
id   └┘     └───────────────┘         └───────────┘└──┘└────┘
src  └┘     └───────────────┘             └───────────┘└──┘└────┘
typ  └┘     └───────────────┘         └───────────┘└──┘└────┘
doc         └───────────────┘
634  have ¬differentiable_at 𝕜 (λ y, -f y) x, from λ h', by simpa only [neg_neg] using h'.neg,
id   └──┘ └───────────────┘                   └┘                 └─────┘        └────┘
src  └──┘ └───────────────┘                               └──────────┘└─────┘└──────┘└────┘
typ  └──┘ └───────────────┘                   └┘     └──────────┘└─────┘└──────┘└────┘
doc        └───────────────┘                                └──────────┘       └──────┘
txt                                                         └──────────┘       └──────┘
par                                                         └──────────┘       └──────┘
pid                                                              └──┘└┘       └────┘
st                                                         └────────────────────────────────┘
635  by simp only [deriv_zero_of_not_differentiable_at h,
id                 └─────────────────────────────────┘ 
src     └─────────┘└─────────────────────────────────┘ └─
typ     └─────────┘└─────────────────────────────────┘└─
doc     └─────────┘                                    └─
txt     └─────────┘                                    └─
par     └─────────┘                                    └─
pid         └──┘└┘                                    └─
st     └──────────────────────────────────────────────────
636    deriv_zero_of_not_differentiable_at this, neg_zero]
id     └─────────────────────────────────┘ └──┘  └──────┘
src  ─┘└─────────────────────────────────┘    └┘└──────┘└─
typ  ─┘└─────────────────────────────────┘└──┘└┘└──────┘└─
doc  ─┘                                       └┘        └─
txt  ─┘                                       └┘        └─
par  ─┘                                       └┘        └─
pid  ─┘                                       └┘        
st   ──────────────────────────────────────────────────────
637  
src  
typ  
doc  
txt  
par  
pid  
st   
638  @[simp] lemma deriv_neg' : deriv (λy, -f y) = (λ x, - deriv f x) :=
id                              └───┘               └───┘  
src                             └───┘                   └───┘
typ                             └───┘               └───┘  
doc    └──┘                     └───┘                      └───┘
639  funext $ λ x, deriv_neg
id   └────┘       └───────┘
src  └────┘        └───────┘
typ  └────┘       └───────┘
640  
641  end neg
642  
643  section sub
644  /-! ### Derivative of the difference of two functions -/
645  
646  theorem has_deriv_at_filter.sub
647    (hf : has_deriv_at_filter f f' x L) (hg : has_deriv_at_filter g g' x L) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
648    has_deriv_at_filter (λ x, f x - g x) (f' - g') x L :=
id     └─────────────────┘             └┘  └┘   
src    └─────────────────┘                     
typ    └─────────────────┘             └┘  └┘   
doc    └─────────────────┘
649  hf.add hg.neg
id   └┘└──┘ └┘└──┘
src    └──┘   └──┘
typ  └┘└──┘ └┘└──┘
650  
651  theorem has_deriv_within_at.sub
652    (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
653    has_deriv_within_at (λ x, f x - g x) (f' - g') s x :=
id     └─────────────────┘             └┘  └┘   
src    └─────────────────┘                     
typ    └─────────────────┘             └┘  └┘   
doc    └─────────────────┘
654  hf.sub hg
id   └┘└──┘ └┘
src    └──┘
typ  └┘└──┘ └┘
655  
656  theorem has_deriv_at.sub
657    (hf : has_deriv_at f f' x) (hg : has_deriv_at g g' x) :
id           └──────────┘  └┘         └──────────┘  └┘ 
src          └──────────┘               └──────────┘
typ          └──────────┘  └┘         └──────────┘  └┘ 
doc          └──────────┘               └──────────┘
658    has_deriv_at (λ x, f x - g x) (f' - g') x :=
id     └──────────┘             └┘  └┘  
src    └──────────┘                     
typ    └──────────┘             └┘  └┘  
doc    └──────────┘
659  hf.sub hg
id   └┘└──┘ └┘
src    └──┘
typ  └┘└──┘ └┘
660  
661  lemma deriv_within_sub (hxs : unique_diff_within_at 𝕜 s x)
id                                 └───────────────────┘   
src                                └───────────────────┘
typ                                └───────────────────┘   
doc                                └───────────────────┘
662    (hf : differentiable_within_at 𝕜 f s x) (hg : differentiable_within_at 𝕜 g s x) :
id           └──────────────────────┘            └──────────────────────┘    
src          └──────────────────────┘                └──────────────────────┘
typ          └──────────────────────┘            └──────────────────────┘    
doc          └──────────────────────┘                └──────────────────────┘
663    deriv_within (λy, f y - g y) s x = deriv_within f s x - deriv_within g s x :=
id     └──────────┘              └──────────┘     └──────────┘   
src    └──────────┘                     └──────────┘        └──────────┘
typ    └──────────┘              └──────────┘     └──────────┘   
doc    └──────────┘                       └──────────┘         └──────────┘
664  (hf.has_deriv_within_at.sub hg.has_deriv_within_at).deriv_within hxs
id    └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
src     └──────────────────┘└──┘   └──────────────────┘ └──────────┘
typ   └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
665  
666  lemma deriv_sub
667    (hf : differentiable_at 𝕜 f x) (hg : differentiable_at 𝕜 g x) :
id           └───────────────┘           └───────────────┘   
src          └───────────────┘              └───────────────┘
typ          └───────────────┘           └───────────────┘   
doc          └───────────────┘              └───────────────┘
668    deriv (λ y, f y - g y) x = deriv f x - deriv g x :=
id     └───┘              └───┘    └───┘  
src    └───┘                    └───┘      └───┘
typ    └───┘              └───┘    └───┘  
doc    └───┘                      └───┘       └───┘
669  (hf.has_deriv_at.sub hg.has_deriv_at).deriv
id    └┘└───────────┘└──┘ └┘└───────────┘ └───┘
src     └───────────┘└──┘   └───────────┘ └───┘
typ   └┘└───────────┘└──┘ └┘└───────────┘ └───┘
670  
671  theorem has_deriv_at_filter.is_O_sub (h : has_deriv_at_filter f f' x L) :
id                                             └─────────────────┘  └┘  
src                                            └─────────────────┘
typ                                            └─────────────────┘  └┘  
doc                                            └─────────────────┘
672    is_O (λ x', f x' - f x) (λ x', x' - x) L :=
id     └──┘    └┘   └┘        └┘  └┘    
src    └──┘                             
typ    └──┘    └┘   └┘        └┘  └┘    
doc    └──┘
673  has_fderiv_at_filter.is_O_sub h
id   └───────────────────────────┘ 
src  └───────────────────────────┘
typ  └───────────────────────────┘ 
674  
675  theorem has_deriv_at_filter.sub_const
676    (hf : has_deriv_at_filter f f' x L) (c : F) :
id           └─────────────────┘  └┘         
src          └─────────────────┘
typ          └─────────────────┘  └┘         
doc          └─────────────────┘
677    has_deriv_at_filter (λ x, f x - c) f' x L :=
id     └─────────────────┘           └┘  
src    └─────────────────┘           
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
678  hf.add_const (-c)
id   └┘└────────┘  
src    └────────┘  
typ  └┘└────────┘  
679  
680  theorem has_deriv_within_at.sub_const
681    (hf : has_deriv_within_at f f' s x) (c : F) :
id           └─────────────────┘  └┘         
src          └─────────────────┘
typ          └─────────────────┘  └┘         
doc          └─────────────────┘
682    has_deriv_within_at (λ x, f x - c) f' s x :=
id     └─────────────────┘           └┘  
src    └─────────────────┘           
typ    └─────────────────┘           └┘  
doc    └─────────────────┘
683  hf.sub_const c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
684  
685  theorem has_deriv_at.sub_const
686    (hf : has_deriv_at f f' x) (c : F) :
id           └──────────┘  └┘        
src          └──────────┘
typ          └──────────┘  └┘        
doc          └──────────┘
687    has_deriv_at (λ x, f x - c) f' x :=
id     └──────────┘           └┘ 
src    └──────────┘           
typ    └──────────┘           └┘ 
doc    └──────────┘
688  hf.sub_const c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
689  
690  lemma deriv_within_sub_const (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
691    (hf : differentiable_within_at 𝕜 f s x) (c : F) :
id           └──────────────────────┘           
src          └──────────────────────┘
typ          └──────────────────────┘           
doc          └──────────────────────┘
692    deriv_within (λy, f y - c) s x = deriv_within f s x :=
id     └──────────┘             └──────────┘   
src    └──────────┘                   └──────────┘
typ    └──────────┘             └──────────┘   
doc    └──────────┘                     └──────────┘
693  (hf.has_deriv_within_at.sub_const c).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
694  
695  lemma deriv_sub_const (c : F) (hf : differentiable_at 𝕜 f x) :
id                                      └───────────────┘   
src                                      └───────────────┘
typ                                     └───────────────┘   
doc                                      └───────────────┘
696    deriv (λ y, f y - c) x = deriv f x :=
id     └───┘             └───┘  
src    └───┘                  └───┘
typ    └───┘             └───┘  
doc    └───┘                    └───┘
697  (hf.has_deriv_at.sub_const c).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
698  
699  theorem has_deriv_at_filter.const_sub (c : F) (hf : has_deriv_at_filter f f' x L) :
id                                                      └─────────────────┘  └┘  
src                                                      └─────────────────┘
typ                                                     └─────────────────┘  └┘  
doc                                                      └─────────────────┘
700    has_deriv_at_filter (λ x, c - f x) (-f') x L :=
id     └─────────────────┘            └┘   
src    └─────────────────┘                
typ    └─────────────────┘            └┘   
doc    └─────────────────┘
701  hf.neg.const_add c
id   └┘└──┘└────────┘ 
src    └──┘└────────┘
typ  └┘└──┘└────────┘ 
702  
703  theorem has_deriv_within_at.const_sub (c : F) (hf : has_deriv_within_at f f' s x) :
id                                                      └─────────────────┘  └┘  
src                                                      └─────────────────┘
typ                                                     └─────────────────┘  └┘  
doc                                                      └─────────────────┘
704    has_deriv_within_at (λ x, c - f x) (-f') s x :=
id     └─────────────────┘            └┘   
src    └─────────────────┘                
typ    └─────────────────┘            └┘   
doc    └─────────────────┘
705  hf.const_sub c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
706  
707  theorem has_deriv_at.const_sub (c : F) (hf : has_deriv_at f f' x) :
id                                               └──────────┘  └┘ 
src                                               └──────────┘
typ                                              └──────────┘  └┘ 
doc                                               └──────────┘
708    has_deriv_at (λ x, c - f x) (-f') x :=
id     └──────────┘            └┘  
src    └──────────┘                
typ    └──────────┘            └┘  
doc    └──────────┘
709  hf.const_sub c
id   └┘└────────┘ 
src    └────────┘
typ  └┘└────────┘ 
710  
711  lemma deriv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
712    (c : F) (hf : differentiable_within_at 𝕜 f s x) :
id                  └──────────────────────┘    
src                  └──────────────────────┘
typ                 └──────────────────────┘    
doc                  └──────────────────────┘
713    deriv_within (λy, c - f y) s x = -deriv_within f s x :=
id     └──────────┘             └──────────┘   
src    └──────────┘                   └──────────┘
typ    └──────────┘             └──────────┘   
doc    └──────────┘                      └──────────┘
714  (hf.has_deriv_within_at.const_sub c).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
715  
716  lemma deriv_const_sub (c : F) (hf : differentiable_at 𝕜 f x) :
id                                      └───────────────┘   
src                                      └───────────────┘
typ                                     └───────────────┘   
doc                                      └───────────────┘
717    deriv (λ y, c - f y) x = -deriv f x :=
id     └───┘             └───┘  
src    └───┘                  └───┘
typ    └───┘             └───┘  
doc    └───┘                     └───┘
718  (hf.has_deriv_at.const_sub c).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
719  
720  end sub
721  
722  section continuous
723  /-! ### Continuity of a function admitting a derivative -/
724  
725  theorem has_deriv_at_filter.tendsto_nhds
726    (hL : L ≤ 𝓝 x) (h : has_deriv_at_filter f f' x L) :
id                     └─────────────────┘  └┘  
src                      └─────────────────┘
typ                    └─────────────────┘  └┘  
doc                       └─────────────────┘
727    tendsto f L (𝓝 (f x)) :=
id     └─────┘       
src    └─────┘      
typ    └─────┘       
doc    └─────┘      
728  has_fderiv_at_filter.tendsto_nhds hL h
id   └───────────────────────────────┘ └┘ 
src  └───────────────────────────────┘
typ  └───────────────────────────────┘ └┘ 
729  
730  theorem has_deriv_within_at.continuous_within_at
731    (h : has_deriv_within_at f f' s x) : continuous_within_at f s x :=
id          └─────────────────┘  └┘      └──────────────────┘   
src         └─────────────────┘             └──────────────────┘
typ         └─────────────────┘  └┘      └──────────────────┘   
doc         └─────────────────┘             └──────────────────┘
732  has_deriv_at_filter.tendsto_nhds lattice.inf_le_left h
id   └──────────────────────────────┘ └─────────────────┘ 
src  └──────────────────────────────┘ └─────────────────┘
typ  └──────────────────────────────┘ └─────────────────┘ 
733  
734  theorem has_deriv_at.continuous_at (h : has_deriv_at f f' x) : continuous_at f x :=
id                                           └──────────┘  └┘     └───────────┘  
src                                          └──────────┘           └───────────┘
typ                                          └──────────┘  └┘     └───────────┘  
doc                                          └──────────┘           └───────────┘
735  has_deriv_at_filter.tendsto_nhds (le_refl _) h
id   └──────────────────────────────┘  └─────┘    
src  └──────────────────────────────┘  └─────┘
typ  └──────────────────────────────┘  └─────┘    
736  
737  end continuous
738  
739  section cartesian_product
740  /-! ### Derivative of the cartesian product of two functions -/
741  
742  variables {G : Type w} [normed_group G] [normed_space 𝕜 G]
id                           └──────────┘     └──────────┘
src                          └──────────┘     └──────────┘
typ                          └──────────┘     └──────────┘
doc                          └──────────┘     └──────────┘
743  variables {f₂ : 𝕜 → G} {f₂' : G}
744  
745  lemma has_deriv_at_filter.prod
746    (hf₁ : has_deriv_at_filter f₁ f₁' x L) (hf₂ : has_deriv_at_filter f₂ f₂' x L) :
id            └─────────────────┘ └┘ └─┘           └─────────────────┘ └┘ └─┘  
src           └─────────────────┘                    └─────────────────┘
typ           └─────────────────┘ └┘ └─┘           └─────────────────┘ └┘ └─┘  
doc           └─────────────────┘                    └─────────────────┘
747    has_deriv_at_filter (λ x, (f₁ x, f₂ x)) (f₁', f₂') x L :=
id     └─────────────────┘      └┘   └┘    └─┘  └─┘   
src    └─────────────────┘                    
typ    └─────────────────┘      └┘   └┘    └─┘  └─┘   
doc    └─────────────────┘
748  show has_fderiv_at_filter _ _ _ _,
id        └──────────────────┘
src       └──────────────────┘
typ       └──────────────────┘
doc       └──────────────────┘
749  by convert has_fderiv_at_filter.prod hf₁ hf₂
id              └───────────────────────┘ └─┘ └─┘
src     └──────┘└───────────────────────┘      
typ     └──────┘└───────────────────────┘└─┘└─┘
doc     └──────┘                               
txt     └──────┘                               
par     └──────┘                               
pid                                           
st     └──────────────────────────────────────────
750  
src  
typ  
doc  
txt  
par  
pid  
st   
751  lemma has_deriv_within_at.prod
752    (hf₁ : has_deriv_within_at f₁ f₁' s x) (hf₂ : has_deriv_within_at f₂ f₂' s x) :
id            └─────────────────┘ └┘ └─┘           └─────────────────┘ └┘ └─┘  
src           └─────────────────┘                    └─────────────────┘
typ           └─────────────────┘ └┘ └─┘           └─────────────────┘ └┘ └─┘  
doc           └─────────────────┘                    └─────────────────┘
753    has_deriv_within_at (λ x, (f₁ x, f₂ x)) (f₁', f₂') s x :=
id     └─────────────────┘      └┘   └┘    └─┘  └─┘   
src    └─────────────────┘                    
typ    └─────────────────┘      └┘   └┘    └─┘  └─┘   
doc    └─────────────────┘
754  hf₁.prod hf₂
id   └─┘└───┘ └─┘
src     └───┘
typ  └─┘└───┘ └─┘
755  
756  lemma has_deriv_at.prod (hf₁ : has_deriv_at f₁ f₁' x) (hf₂ : has_deriv_at f₂ f₂' x) :
id                                  └──────────┘ └┘ └─┘          └──────────┘ └┘ └─┘ 
src                                 └──────────┘                  └──────────┘
typ                                 └──────────┘ └┘ └─┘          └──────────┘ └┘ └─┘ 
doc                                 └──────────┘                  └──────────┘
757    has_deriv_at (λ x, (f₁ x, f₂ x)) (f₁', f₂') x :=
id     └──────────┘      └┘   └┘    └─┘  └─┘  
src    └──────────┘                    
typ    └──────────┘      └┘   └┘    └─┘  └─┘  
doc    └──────────┘
758  hf₁.prod hf₂
id   └─┘└───┘ └─┘
src     └───┘
typ  └─┘└───┘ └─┘
759  
760  end cartesian_product
761  
762  section composition
763  /-! ### Derivative of the composition of a vector valued function and a scalar function -/
764  
765  variables {h : 𝕜 → 𝕜} {h' : 𝕜}
766  /- For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to
767  get confused since there are too many possibilities for composition -/
768  variable (x)
769  
770  theorem has_deriv_at_filter.comp
771    (hg : has_deriv_at_filter g g' (h x) (L.map h))
id           └─────────────────┘  └┘      └──┘ 
src          └─────────────────┘              └──┘
typ          └─────────────────┘  └┘      └──┘ 
doc          └─────────────────┘              └──┘
772    (hh : has_deriv_at_filter h h' x L) :
id           └─────────────────┘  └┘  
src          └─────────────────┘
typ          └─────────────────┘  └┘  
doc          └─────────────────┘
773    has_deriv_at_filter (g ∘ h) (h' • g') x L :=
id     └─────────────────┘       └┘  └┘   
src    └─────────────────┘            
typ    └─────────────────┘       └┘  └┘   
doc    └─────────────────┘
774  have (smul_right 1 g' : 𝕜 →L[𝕜] _).comp
id         └────────┘   └┘    └─┘   └──┘
src        └────────┘          └─┘    └──┘
typ        └────────┘   └┘    └─┘   └──┘
doc        └────────┘          └─┘    └──┘
775        (smul_right 1 h' : 𝕜 →L[𝕜] _) =
id          └────────┘   └┘    └─┘    
src         └────────┘          └─┘     
typ         └────────┘   └┘    └─┘    
doc         └────────┘          └─┘ 
776      smul_right 1 (h' • g'), by { ext, simp [mul_smul] },
id       └────────┘    └┘  └┘                   └──────┘
src      └────────┘                  └─┘  └────┘└──────┘└┘
typ      └────────┘    └┘  └┘        └─┘  └────┘└──────┘└┘
doc      └────────┘                   └─┘  └────┘        └┘
txt                                   └─┘  └────┘        └┘
par                                   └─┘  └────┘        └┘
pid                                                    
st                                 └────┘└────────────────┘└┘
777  begin
st   └─────
778    unfold has_deriv_at_filter,
src    └────────────────────────┘
typ    └────────────────────────┘
doc    └────────────────────────┘
txt    └────────────────────────┘
par    └────────────────────────┘
pid          └──────────────────┘
st   ───────────────────────────┘└─
779    rw ← this,
id          └──┘
src    └───┘
typ    └───┘└──┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────┘└─
780    exact has_fderiv_at_filter.comp x hg hh,
id           └───────────────────────┘  └┘ └┘
src    └────┘└───────────────────────┘   
typ    └────┘└───────────────────────┘└┘└┘
doc    └────┘                            
txt    └────┘                            
par    └────┘                            
pid                                     
st   ────────────────────────────────────────┘└─
781  end
st   ──┘
782  
783  theorem has_deriv_within_at.comp {t : set 𝕜}
id                                         └─┘ 
src                                        └─┘
typ                                        └─┘ 
784    (hg : has_deriv_within_at g g' t (h x))
id           └─────────────────┘  └┘    
src          └─────────────────┘
typ          └─────────────────┘  └┘    
doc          └─────────────────┘
785    (hh : has_deriv_within_at h h' s x) (hst : s ⊆ h ⁻¹' t) :
id           └─────────────────┘  └┘              └─┘ 
src          └─────────────────┘                       └─┘
typ          └─────────────────┘  └┘              └─┘ 
doc          └─────────────────┘                        └─┘
786    has_deriv_within_at (g ∘ h) (h' • g') s x :=
id     └─────────────────┘       └┘  └┘   
src    └─────────────────┘            
typ    └─────────────────┘       └┘  └┘   
doc    └─────────────────┘
787  begin
st   └─────
788    apply has_deriv_at_filter.comp _ (has_deriv_at_filter.mono hg _) hh,
id           └──────────────────────┘    └──────────────────────┘ └┘    └┘
src    └────┘└──────────────────────┘└─┘ └──────────────────────┘  └──┘
typ    └────┘└──────────────────────┘└─┘ └──────────────────────┘└┘└──┘└┘
doc    └────┘                        └─┘                           └──┘
txt    └────┘                        └─┘                           └──┘
par    └────┘                        └─┘                           └──┘
pid                                 └─┘                           └──┘
st   ────────────────────────────────────────────────────────────────────┘└─
789    calc map h (nhds_within x s)
id     └──┘ └─┘
src    └──┘ └─┘
typ    └──┘ └─┘
doc    └──┘ └─┘
st   ───────────────────────────────
790        ≤ nhds_within (h x) (h '' s) : hh.continuous_within_at.tendsto_nhds_within_image
id                                └┘     └───────────────────────────────────────────────┘
src                               └┘      └───────────────────────────────────────────────┘
typ                               └┘     └───────────────────────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────
791    ... ≤ nhds_within (h x) t        : nhds_within_mono _ (image_subset_iff.mpr hst)
id           └─────────┘               └──────────────┘    └──────────────────┘ └─┘
src          └─────────┘                  └──────────────┘    └──────────────────┘
typ          └─────────┘               └──────────────┘    └──────────────────┘ └─┘
doc          └─────────┘                                      └──────────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────┘
792  end
st   ──┘
793  
794  /-- The chain rule. -/
795  theorem has_deriv_at.comp
796    (hg : has_deriv_at g g' (h x)) (hh : has_deriv_at h h' x) :
id           └──────────┘  └┘            └──────────┘  └┘ 
src          └──────────┘                   └──────────┘
typ          └──────────┘  └┘            └──────────┘  └┘ 
doc          └──────────┘                   └──────────┘
797    has_deriv_at (g ∘ h) (h' • g') x :=
id     └──────────┘       └┘  └┘  
src    └──────────┘            
typ    └──────────┘       └┘  └┘  
doc    └──────────┘
798  (hg.mono hh.continuous_at).comp x hh
id    └┘└───┘ └┘└────────────┘ └──┘   └┘
src     └───┘   └────────────┘ └──┘
typ   └┘└───┘ └┘└────────────┘ └──┘   └┘
799  
800  theorem has_deriv_at.comp_has_deriv_within_at
801    (hg : has_deriv_at g g' (h x)) (hh : has_deriv_within_at h h' s x) :
id           └──────────┘  └┘            └─────────────────┘  └┘  
src          └──────────┘                   └─────────────────┘
typ          └──────────┘  └┘            └─────────────────┘  └┘  
doc          └──────────┘                   └─────────────────┘
802    has_deriv_within_at (g ∘ h) (h' • g') s x :=
id     └─────────────────┘       └┘  └┘   
src    └─────────────────┘            
typ    └─────────────────┘       └┘  └┘   
doc    └─────────────────┘
803  begin
st   └─────
804    rw ← has_deriv_within_at_univ at hg,
id          └──────────────────────┘
src    └───┘└──────────────────────┘└────┘
typ    └───┘└──────────────────────┘└────┘
doc    └───┘                        └────┘
txt    └───┘                        └────┘
par    └───┘                        └────┘
pid      └─┘                        └────┘
st   ────────────────────────────────────┘└─
805    exact has_deriv_within_at.comp x hg hh subset_preimage_univ
id           └──────────────────────┘  └┘ └┘ └──────────────────┘
src    └────┘└──────────────────────┘     └──────────────────┘
typ    └────┘└──────────────────────┘└┘└┘└──────────────────┘
doc    └────┘                                                 
txt    └────┘                                                 
par    └────┘                                                 
pid                                                          
st   ─────────────────────────────────────────────────────────────┘
806  end
st   └─┘
807  
808  lemma deriv_within.comp
809    (hg : differentiable_within_at 𝕜 g t (h x)) (hh : differentiable_within_at 𝕜 h s x)
id           └──────────────────────┘               └──────────────────────┘    
src          └──────────────────────┘                    └──────────────────────┘
typ          └──────────────────────┘               └──────────────────────┘    
doc          └──────────────────────┘                    └──────────────────────┘
810    (hs : s ⊆ h ⁻¹' t) (hxs : unique_diff_within_at 𝕜 s x) :
id              └─┘          └───────────────────┘   
src               └─┘           └───────────────────┘
typ             └─┘          └───────────────────┘   
doc                └─┘           └───────────────────┘
811    deriv_within (g ∘ h) s x = deriv_within h s x • deriv_within g t (h x) :=
id     └──────────┘         └──────────┘     └──────────┘     
src    └──────────┘             └──────────┘        └──────────┘
typ    └──────────┘         └──────────┘     └──────────┘     
doc    └──────────┘               └──────────┘         └──────────┘
812  begin
st   └─────
813    apply has_deriv_within_at.deriv_within _ hxs,
id           └──────────────────────────────┘   └─┘
src    └────┘└──────────────────────────────┘└─┘
typ    └────┘└──────────────────────────────┘└─┘└─┘
doc    └────┘                                └─┘
txt    └────┘                                └─┘
par    └────┘                                └─┘
pid                                         └─┘
st   ─────────────────────────────────────────────┘└─
814    exact has_deriv_within_at.comp x (hg.has_deriv_within_at) (hh.has_deriv_within_at) hs
id           └──────────────────────┘   └────────────────────┘   └────────────────────┘  └┘
src    └────┘└──────────────────────┘  └────────────────────┘└┘ └────────────────────┘└┘  
typ    └────┘└──────────────────────┘ └────────────────────┘└┘ └────────────────────┘└┘└┘
doc    └────┘                                                └┘                       └┘  
txt    └────┘                                                └┘                       └┘  
par    └────┘                                                └┘                       └┘  
pid                                                         └┘                       └┘  
st   ───────────────────────────────────────────────────────────────────────────────────────┘
815  end
st   └─┘
816  
817  lemma deriv.comp
818    (hg : differentiable_at 𝕜 g (h x)) (hh : differentiable_at 𝕜 h x) :
id           └───────────────┘              └───────────────┘   
src          └───────────────┘                  └───────────────┘
typ          └───────────────┘              └───────────────┘   
doc          └───────────────┘                  └───────────────┘
819    deriv (g ∘ h) x = deriv h x • deriv g (h x) :=
id     └───┘        └───┘    └───┘    
src    └───┘           └───┘      └───┘
typ    └───┘        └───┘    └───┘    
doc    └───┘             └───┘       └───┘
820  begin
st   └─────
821    apply has_deriv_at.deriv,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
822    exact has_deriv_at.comp x hg.has_deriv_at hh.has_deriv_at
id           └───────────────┘  └─────────────┘ └─────────────┘
src    └────┘└───────────────┘ └─────────────┘└─────────────┘
typ    └────┘└───────────────┘└─────────────┘└─────────────┘
doc    └────┘└───────────────┘                               
txt    └────┘                                                
par    └────┘                                                
pid                                                         
st   ───────────────────────────────────────────────────────────┘
823  end
st   └─┘
824  
825  end composition
826  
827  section composition_vector
828  /-! ### Derivative of the composition of a function between vector spaces and of a function defined on `𝕜` -/
829  
830  variables {l : F → E} {l' : F →L[𝕜] E}
id                                 └─┘ 
src                                └─┘ 
typ                                └─┘ 
doc                                └─┘ 
831  variable (x)
832  
833  /-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
834  equal to the Fréchet derivative of `l` applied to the derivative of `f`. -/
835  theorem has_fderiv_within_at.comp_has_deriv_within_at {t : set F}
id                                                              └─┘ 
src                                                             └─┘
typ                                                             └─┘ 
836    (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x) (hst : s ⊆ f ⁻¹' t) :
id           └──────────────────┘  └┘             └─────────────────┘  └┘              └─┘ 
src          └──────────────────┘                     └─────────────────┘                       └─┘
typ          └──────────────────┘  └┘             └─────────────────┘  └┘              └─┘ 
doc          └──────────────────┘                     └─────────────────┘                        └─┘
837    has_deriv_within_at (l ∘ f) (l' (f')) s x :=
id     └─────────────────┘       └┘  └┘    
src    └─────────────────┘    
typ    └─────────────────┘       └┘  └┘    
doc    └─────────────────┘
838  begin
st   └─────
839    rw has_deriv_within_at_iff_has_fderiv_within_at,
id        └──────────────────────────────────────────┘
src    └─┘└──────────────────────────────────────────┘
typ    └─┘└──────────────────────────────────────────┘
doc    └─┘└──────────────────────────────────────────┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────────────────────────────────┘└─
840    convert has_fderiv_within_at.comp x hl hf hst,
id             └───────────────────────┘  └┘ └┘ └─┘
src    └──────┘└───────────────────────┘     
typ    └──────┘└───────────────────────┘└┘└┘└─┘
doc    └──────┘                              
txt    └──────┘                              
par    └──────┘                              
pid                                         
st   ──────────────────────────────────────────────┘└─
841    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
842    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
843  end
st   └─┘
844  
845  /-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
846  Fréchet derivative of `l` applied to the derivative of `f`. -/
847  theorem has_fderiv_at.comp_has_deriv_at
848    (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_at f f' x) :
id           └───────────┘  └┘            └──────────┘  └┘ 
src          └───────────┘                   └──────────┘
typ          └───────────┘  └┘            └──────────┘  └┘ 
doc          └───────────┘                   └──────────┘
849    has_deriv_at (l ∘ f) (l' (f')) x :=
id     └──────────┘       └┘  └┘   
src    └──────────┘    
typ    └──────────┘       └┘  └┘   
doc    └──────────┘
850  begin
st   └─────
851    rw has_deriv_at_iff_has_fderiv_at,
id        └────────────────────────────┘
src    └─┘└────────────────────────────┘
typ    └─┘└────────────────────────────┘
doc    └─┘└────────────────────────────┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────────────┘└─
852    convert has_fderiv_at.comp x hl hf,
id             └────────────────┘  └┘ └┘
src    └──────┘└────────────────┘   
typ    └──────┘└────────────────┘└┘└┘
doc    └──────┘└────────────────┘   
txt    └──────┘                     
par    └──────┘                     
pid                                
st   ───────────────────────────────────┘└─
853    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
854    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
855  end
st   └─┘
856  
857  theorem has_fderiv_at.comp_has_deriv_within_at
858    (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) :
id           └───────────┘  └┘            └─────────────────┘  └┘  
src          └───────────┘                   └─────────────────┘
typ          └───────────┘  └┘            └─────────────────┘  └┘  
doc          └───────────┘                   └─────────────────┘
859    has_deriv_within_at (l ∘ f) (l' (f')) s x :=
id     └─────────────────┘       └┘  └┘    
src    └─────────────────┘    
typ    └─────────────────┘       └┘  └┘    
doc    └─────────────────┘
860  begin
st   └─────
861    rw ← has_fderiv_within_at_univ at hl,
id          └───────────────────────┘
src    └───┘└───────────────────────┘└────┘
typ    └───┘└───────────────────────┘└────┘
doc    └───┘                         └────┘
txt    └───┘                         └────┘
par    └───┘                         └────┘
pid      └─┘                         └────┘
st   ─────────────────────────────────────┘└─
862    exact has_fderiv_within_at.comp_has_deriv_within_at x hl hf subset_preimage_univ
id           └───────────────────────────────────────────┘  └┘ └┘ └──────────────────┘
src    └────┘└───────────────────────────────────────────┘     └──────────────────┘
typ    └────┘└───────────────────────────────────────────┘└┘└┘└──────────────────┘
doc    └────┘└───────────────────────────────────────────┘                         
txt    └────┘                                                                      
par    └────┘                                                                      
pid                                                                               
st   ──────────────────────────────────────────────────────────────────────────────────┘
863  end
st   └─┘
864  
865  lemma fderiv_within.comp_deriv_within {t : set F}
id                                              └─┘ 
src                                             └─┘
typ                                             └─┘ 
866    (hl : differentiable_within_at 𝕜 l t (f x)) (hf : differentiable_within_at 𝕜 f s x)
id           └──────────────────────┘               └──────────────────────┘    
src          └──────────────────────┘                    └──────────────────────┘
typ          └──────────────────────┘               └──────────────────────┘    
doc          └──────────────────────┘                    └──────────────────────┘
867    (hs : s ⊆ f ⁻¹' t) (hxs : unique_diff_within_at 𝕜 s x) :
id              └─┘          └───────────────────┘   
src               └─┘           └───────────────────┘
typ             └─┘          └───────────────────┘   
doc                └─┘           └───────────────────┘
868    deriv_within (l ∘ f) s x = (fderiv_within 𝕜 l t (f x) : F → E) (deriv_within f s x) :=
id     └──────────┘          └───────────┘                └──────────┘   
src    └──────────┘              └───────────┘                       └──────────┘
typ    └──────────┘          └───────────┘                └──────────┘   
doc    └──────────┘                └───────────┘                       └──────────┘
869  begin
st   └─────
870    apply has_deriv_within_at.deriv_within _ hxs,
id           └──────────────────────────────┘   └─┘
src    └────┘└──────────────────────────────┘└─┘
typ    └────┘└──────────────────────────────┘└─┘└─┘
doc    └────┘                                └─┘
txt    └────┘                                └─┘
par    └────┘                                └─┘
pid                                         └─┘
st   ─────────────────────────────────────────────┘└─
871    exact (hl.has_fderiv_within_at).comp_has_deriv_within_at x (hf.has_deriv_within_at) hs
id            └─────────────────────┘                             └────────────────────┘  └┘
src    └────┘ └─────────────────────┘└─────────────────────────┘  └────────────────────┘└┘  
typ    └────┘ └─────────────────────┘└─────────────────────────┘ └────────────────────┘└┘└┘
doc    └────┘                        └─────────────────────────┘                        └┘  
txt    └────┘                        └─────────────────────────┘                        └┘  
par    └────┘                        └─────────────────────────┘                        └┘  
pid                                 └─────────────────────────┘                        └┘  
st   ────────────────────────────────────────────────────────────────────────────────────────┘
872  end
st   └─┘
873  
874  lemma fderiv.comp_deriv
875    (hl : differentiable_at 𝕜 l (f x)) (hf : differentiable_at 𝕜 f x) :
id           └───────────────┘              └───────────────┘   
src          └───────────────┘                  └───────────────┘
typ          └───────────────┘              └───────────────┘   
doc          └───────────────┘                  └───────────────┘
876    deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x) :=
id     └───┘         └────┘               └───┘  
src    └───┘            └────┘                     └───┘
typ    └───┘         └────┘               └───┘  
doc    └───┘              └────┘                     └───┘
877  begin
st   └─────
878    apply has_deriv_at.deriv _,
id           └────────────────┘
src    └────┘└────────────────┘└┘
typ    └────┘└────────────────┘└┘
doc    └────┘                  └┘
txt    └────┘                  └┘
par    └────┘                  └┘
pid                           └┘
st   ───────────────────────────┘└─
879    exact (hl.has_fderiv_at).comp_has_deriv_at x (hf.has_deriv_at)
id            └──────────────┘                      └─────────────┘
src    └────┘ └──────────────┘└──────────────────┘  └─────────────┘└┘
typ    └────┘ └──────────────┘└──────────────────┘ └─────────────┘└┘
doc    └────┘                 └──────────────────┘                 └┘
txt    └────┘                 └──────────────────┘                 └┘
par    └────┘                 └──────────────────┘                 └┘
pid                          └──────────────────┘                 
st   ────────────────────────────────────────────────────────────────┘
880  end
st   └─┘
881  
882  end composition_vector
883  
884  section mul
885  /-! ### Derivative of the multiplication of two scalar functions -/
886  variables {c d : 𝕜 → 𝕜} {c' d' : 𝕜}
887  
888  theorem has_deriv_within_at.mul
889    (hc : has_deriv_within_at c c' s x) (hd : has_deriv_within_at d d' s x) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘  
src          └─────────────────┘                 └─────────────────┘
typ          └─────────────────┘  └┘          └─────────────────┘  └┘  
doc          └─────────────────┘                 └─────────────────┘
890    has_deriv_within_at (λ y, c y * d y) (c' * d x + c x * d') s x :=
id     └─────────────────┘             └┘        └┘   
src    └─────────────────┘                               
typ    └─────────────────┘             └┘        └┘   
doc    └─────────────────┘
891  begin
st   └─────
892    convert hc.smul hd using 1,
id             └─────┘ └┘
src    └──────┘└─────┘  └──────┘
typ    └──────┘└─────┘└┘└──────┘
doc    └──────┘         └──────┘
txt    └──────┘         └──────┘
par    └──────┘         └──────┘
pid                    └─────┘
st   ───────────────────────────┘└─
893    rw [smul_eq_mul, smul_eq_mul, add_comm]
id         └─────────┘  └─────────┘  └──────┘
src    └──┘└─────────┘└┘└─────────┘└┘└──────┘└┘
typ    └──┘└─────────┘└┘└─────────┘└┘└──────┘└┘
doc    └──┘           └┘           └┘        └┘
txt    └──┘           └┘           └┘        └┘
par    └──┘           └┘           └┘        └┘
pid      └┘           └┘           └┘        
st   ────────────────┘└───────────┘└────────┘
894  end
st   └─┘
895  
896  theorem has_deriv_at.mul (hc : has_deriv_at c c' x) (hd : has_deriv_at d d' x) :
id                                  └──────────┘  └┘         └──────────┘  └┘ 
src                                 └──────────┘               └──────────┘
typ                                 └──────────┘  └┘         └──────────┘  └┘ 
doc                                 └──────────┘               └──────────┘
897    has_deriv_at (λ y, c y * d y) (c' * d x + c x * d') x :=
id     └──────────┘             └┘        └┘  
src    └──────────┘                               
typ    └──────────┘             └┘        └┘  
doc    └──────────┘
898  begin
st   └─────
899    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
900    exact hc.mul hd
id           └────┘ └┘
src    └────┘└────┘  
typ    └────┘└────┘└┘
doc    └────┘        
txt    └────┘        
par    └────┘        
pid                 
st   ─────────────────┘
901  end
st   └─┘
902  
903  lemma deriv_within_mul (hxs : unique_diff_within_at 𝕜 s x)
id                                 └───────────────────┘   
src                                └───────────────────┘
typ                                └───────────────────┘   
doc                                └───────────────────┘
904    (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) :
id           └──────────────────────┘            └──────────────────────┘    
src          └──────────────────────┘                └──────────────────────┘
typ          └──────────────────────┘            └──────────────────────┘    
doc          └──────────────────────┘                └──────────────────────┘
905    deriv_within (λ y, c y * d y) s x = deriv_within c s x * d x + c x * deriv_within d s x :=
id     └──────────┘               └──────────┘           └──────────┘   
src    └──────────┘                      └──────────┘                  └──────────┘
typ    └──────────┘               └──────────┘           └──────────┘   
doc    └──────────┘                        └──────────┘                     └──────────┘
906  (hc.has_deriv_within_at.mul hd.has_deriv_within_at).deriv_within hxs
id    └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
src     └──────────────────┘└──┘   └──────────────────┘ └──────────┘
typ   └┘└──────────────────┘└──┘ └┘└──────────────────┘ └──────────┘  └─┘
907  
908  lemma deriv_mul (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜 d x) :
id                         └───────────────┘           └───────────────┘   
src                        └───────────────┘              └───────────────┘
typ                        └───────────────┘           └───────────────┘   
doc                        └───────────────┘              └───────────────┘
909    deriv (λ y, c y * d y) x = deriv c x * d x + c x * deriv d x :=
id     └───┘              └───┘          └───┘  
src    └───┘                    └───┘                └───┘
typ    └───┘              └───┘          └───┘  
doc    └───┘                      └───┘                   └───┘
910  (hc.has_deriv_at.mul hd.has_deriv_at).deriv
id    └┘└───────────┘└──┘ └┘└───────────┘ └───┘
src     └───────────┘└──┘   └───────────┘ └───┘
typ   └┘└───────────┘└──┘ └┘└───────────┘ └───┘
911  
912  theorem has_deriv_within_at.mul_const (hc : has_deriv_within_at c c' s x) (d : 𝕜) :
id                                               └─────────────────┘  └┘         
src                                              └─────────────────┘
typ                                              └─────────────────┘  └┘         
doc                                              └─────────────────┘
913    has_deriv_within_at (λ y, c y * d) (c' * d) s x :=
id     └─────────────────┘            └┘     
src    └─────────────────┘                   
typ    └─────────────────┘            └┘     
doc    └─────────────────┘
914  begin
st   └─────
915    convert hc.mul (has_deriv_within_at_const x s d),
id             └────┘  └───────────────────────┘   
src    └──────┘└────┘ └───────────────────────┘   
typ    └──────┘└────┘ └───────────────────────┘
doc    └──────┘                                   
txt    └──────┘                                   
par    └──────┘                                   
pid                                              
st   ─────────────────────────────────────────────────┘└─
916    rw [mul_zero, add_zero]
id         └──────┘  └──────┘
src    └──┘└──────┘└┘└──────┘└┘
typ    └──┘└──────┘└┘└──────┘└┘
doc    └──┘        └┘        └┘
txt    └──┘        └┘        └┘
par    └──┘        └┘        └┘
pid      └┘        └┘        
st   ─────────────┘└────────┘
917  end
st   └─┘
918  
919  theorem has_deriv_at.mul_const (hc : has_deriv_at c c' x) (d : 𝕜) :
id                                        └──────────┘  └┘        
src                                       └──────────┘
typ                                       └──────────┘  └┘        
doc                                       └──────────┘
920    has_deriv_at (λ y, c y * d) (c' * d) x :=
id     └──────────┘            └┘    
src    └──────────┘                   
typ    └──────────┘            └┘    
doc    └──────────┘
921  begin
st   └─────
922    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
923    exact hc.mul_const d
id           └──────────┘ 
src    └────┘└──────────┘ 
typ    └────┘└──────────┘
doc    └────┘             
txt    └────┘             
par    └────┘             
pid                      
st   ──────────────────────┘
924  end
st   └─┘
925  
926  lemma deriv_within_mul_const (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
927    (hc : differentiable_within_at 𝕜 c s x) (d : 𝕜) :
id           └──────────────────────┘           
src          └──────────────────────┘
typ          └──────────────────────┘           
doc          └──────────────────────┘
928    deriv_within (λ y, c y * d) s x = deriv_within c s x * d :=
id     └──────────┘              └──────────┘     
src    └──────────┘                    └──────────┘       
typ    └──────────┘              └──────────┘     
doc    └──────────┘                      └──────────┘
929  (hc.has_deriv_within_at.mul_const d).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
930  
931  lemma deriv_mul_const (hc : differentiable_at 𝕜 c x) (d : 𝕜) :
id                               └───────────────┘          
src                              └───────────────┘
typ                              └───────────────┘          
doc                              └───────────────┘
932    deriv (λ y, c y * d) x = deriv c x * d :=
id     └───┘             └───┘    
src    └───┘                  └───┘     
typ    └───┘             └───┘    
doc    └───┘                    └───┘
933  (hc.has_deriv_at.mul_const d).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
934  
935  theorem has_deriv_within_at.const_mul (c : 𝕜) (hd : has_deriv_within_at d d' s x) :
id                                                      └─────────────────┘  └┘  
src                                                      └─────────────────┘
typ                                                     └─────────────────┘  └┘  
doc                                                      └─────────────────┘
936    has_deriv_within_at (λ y, c * d y) (c * d') s x :=
id     └─────────────────┘              └┘   
src    └─────────────────┘                  
typ    └─────────────────┘              └┘   
doc    └─────────────────┘
937  begin
st   └─────
938    convert (has_deriv_within_at_const x s c).mul hd,
id              └───────────────────────┘         └┘
src    └──────┘ └───────────────────────┘   └────┘
typ    └──────┘ └───────────────────────┘└────┘└┘
doc    └──────┘                             └────┘
txt    └──────┘                             └────┘
par    └──────┘                             └────┘
pid                                        └────┘
st   ─────────────────────────────────────────────────┘└─
939    rw [zero_mul, zero_add]
id         └──────┘  └──────┘
src    └──┘└──────┘└┘└──────┘└┘
typ    └──┘└──────┘└┘└──────┘└┘
doc    └──┘        └┘        └┘
txt    └──┘        └┘        └┘
par    └──┘        └┘        └┘
pid      └┘        └┘        
st   ─────────────┘└────────┘
940  end
st   └─┘
941  
942  theorem has_deriv_at.const_mul (c : 𝕜) (hd : has_deriv_at d d' x) :
id                                               └──────────┘  └┘ 
src                                               └──────────┘
typ                                              └──────────┘  └┘ 
doc                                               └──────────┘
943    has_deriv_at (λ y, c * d y) (c * d') x :=
id     └──────────┘              └┘  
src    └──────────┘                  
typ    └──────────┘              └┘  
doc    └──────────┘
944  begin
st   └─────
945    rw [← has_deriv_within_at_univ] at *,
id           └──────────────────────┘
src    └────┘└──────────────────────┘└────┘
typ    └────┘└──────────────────────┘└────┘
doc    └────┘                        └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid      └──┘                        └───┘
st   ───────────────────────────────┘└───┘└─
946    exact hd.const_mul c
id           └──────────┘ 
src    └────┘└──────────┘ 
typ    └────┘└──────────┘
doc    └────┘             
txt    └────┘             
par    └────┘             
pid                      
st   ──────────────────────┘
947  end
st   └─┘
948  
949  lemma deriv_within_const_mul (hxs : unique_diff_within_at 𝕜 s x)
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
950    (c : 𝕜) (hd : differentiable_within_at 𝕜 d s x) :
id                  └──────────────────────┘    
src                  └──────────────────────┘
typ                 └──────────────────────┘    
doc                  └──────────────────────┘
951    deriv_within (λ y, c * d y) s x = c * deriv_within d s x :=
id     └──────────┘                └──────────┘   
src    └──────────┘                       └──────────┘
typ    └──────────┘                └──────────┘   
doc    └──────────┘                          └──────────┘
952  (hd.has_deriv_within_at.const_mul c).deriv_within hxs
id    └┘└──────────────────┘└────────┘  └──────────┘  └─┘
src     └──────────────────┘└────────┘   └──────────┘
typ   └┘└──────────────────┘└────────┘  └──────────┘  └─┘
953  
954  lemma deriv_const_mul (c : 𝕜) (hd : differentiable_at 𝕜 d x) :
id                                      └───────────────┘   
src                                      └───────────────┘
typ                                     └───────────────┘   
doc                                      └───────────────┘
955    deriv (λ y, c * d y) x = c * deriv d x :=
id     └───┘               └───┘  
src    └───┘                     └───┘
typ    └───┘               └───┘  
doc    └───┘                        └───┘
956  (hd.has_deriv_at.const_mul c).deriv
id    └┘└───────────┘└────────┘  └───┘
src     └───────────┘└────────┘   └───┘
typ   └┘└───────────┘└────────┘  └───┘
957  
958  end mul
959  
960  section inverse
961  /-! ### Derivative of `x ↦ x⁻¹` -/
962  
963  lemma has_deriv_at_inv_one :
964    has_deriv_at (λx, x⁻¹) (-1) (1 : 𝕜) :=
id     └──────────┘     └┘           
src    └──────────┘       └┘   
typ    └──────────┘     └┘           
doc    └──────────┘
965  begin
st   └─────
966    rw has_deriv_at_iff_is_o_nhds_zero,
id        └─────────────────────────────┘
src    └─┘└─────────────────────────────┘
typ    └─┘└─────────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────────────────┘└─
967    have : is_o (λ (h : 𝕜), h^2 * (1 + h)⁻¹) (λ (h : 𝕜), h * 1) (𝓝 0),
id            └──┘                       └┘                     
src    └─────┘└──┘  └────┘ └─┘ └┘ └┘ └┘└┘  └────┘ └─┘  └──┘ └─┘
typ    └─────┘└──┘  └────┘ └─┘ └┘ └┘ └┘└┘  └────┘└─┘  └──┘ └─┘
doc    └─────┘└──┘  └────┘ └─┘  └┘  └┘    └┘  └────┘ └─┘  └──┘ └─┘
txt    └─────┘      └────┘ └─┘  └┘  └┘    └┘  └────┘ └─┘  └──┘  └─┘
par    └─────┘      └────┘ └─┘  └┘  └┘    └┘  └────┘ └─┘  └──┘  └─┘
pid    └───┘└┘      └────┘ └─┘  └┘  └┘    └┘  └────┘ └─┘  └──┘  └─┘
st   ──────────────────────────────────────────────────────────────────┘└─
968    { have : tendsto (λ (h : 𝕜), (1 + h)⁻¹) (𝓝 0) (𝓝 (1 + 0)⁻¹) :=
id              └─────┘         
src      └─────┘└─────┘  └────┘ └─┘ └┘    └┘  └──┘   └┘ └─┘  └────
typ      └─────┘└─────┘  └────┘└─┘ └┘    └┘  └──┘   └┘ └─┘  └────
doc      └─────┘└─────┘  └────┘ └─┘ └┘    └┘  └──┘   └┘ └─┘  └────
txt      └─────┘         └────┘ └─┘ └┘    └┘  └──┘   └┘ └─┘  └────
par      └─────┘         └────┘ └─┘ └┘    └┘  └──┘   └┘ └─┘  └────
pid      └───┘└┘         └────┘ └─┘ └┘    └┘  └──┘   └┘ └─┘  └───
st   ───┘└────────────────────────────────────────────────────────────
969        ((tendsto_const_nhds).add tendsto_id).inv' (by norm_num),
id           └────────────────┘      └────────┘
src  ─────┘  └────────────────┘└────┘└────────┘└─────┘   └──────┘
typ  ─────┘  └────────────────┘└────┘└────────┘└─────┘   └──────┘
doc  ─────┘                    └────┘          └─────┘   └──────┘
txt  ─────┘                    └────┘          └─────┘   └──────┘
par  ─────┘                    └────┘          └─────┘   └──────┘
pid  ─────┘                    └────┘          └─────┘   └────────┘
st   ───────────────────────────────────────────────────┘└───────┘└─
970      exact is_o.mul_is_O (is_o_pow_id one_lt_two) (is_O_one_of_tendsto _ this) },
id             └───────────┘  └─────────┘ └────────┘   └─────────────────┘   └──┘
src      └────┘└───────────┘ └─────────┘└────────┘└┘ └─────────────────┘└─┘    └┘
typ      └────┘└───────────┘ └─────────┘└────────┘└┘ └─────────────────┘└─┘└──┘└┘
doc      └────┘                                   └┘                    └─┘    └┘
txt      └────┘                                   └┘                    └─┘    └┘
par      └────┘                                   └┘                    └─┘    └┘
pid                                              └┘                    └─┘    
st   ─────────────────────────────────────────────────────────────────────────────┘└┘
971    apply this.congr' _ _,
id           └─────────┘
src    └────┘└─────────┘└──┘
typ    └────┘└─────────┘└──┘
doc    └────┘           └──┘
txt    └────┘           └──┘
par    └────┘           └──┘
pid                    └──┘
st   ──────────────────────┘└─
972    { have : metric.ball (0 : 𝕜) 1 ∈ 𝓝 (0 : 𝕜),
id              └─────────┘                   
src      └─────┘└─────────┘ └──┘ └──┘  └──┘ 
typ      └─────┘└─────────┘ └──┘ └──┘  └──┘
doc      └─────┘└─────────┘ └──┘ └──┘   └──┘ 
txt      └─────┘            └──┘ └──┘   └──┘ 
par      └─────┘            └──┘ └──┘   └──┘ 
pid      └───┘└┘            └──┘ └──┘   └──┘ 
st   ───┘└──────────────────────────────────────┘└─
973        from metric.ball_mem_nhds 0 zero_lt_one,
id              └──────────────────┘   └─────────┘
src        └───┘└──────────────────┘└─┘└─────────┘
typ        └───┘└──────────────────┘└─┘└─────────┘
doc        └───┘                    └─┘
txt        └───┘                    └─┘
par        └───┘                    └─┘
pid        └───┘                    └─┘
st   ────────────────────────────────────────────┘└─
974      filter_upwards [this],
src      └──────────────┘    
typ      └──────────────┘    
doc      └──────────────┘    
txt      └──────────────┘    
par      └──────────────┘    
pid                    └┘    
st   ────────────────────────┘└─
975      assume h hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
976      have : 0 < ∥1 + h∥ := calc
id                     
src      └───────┘└┘  └──┘    
typ      └───────┘└┘ └──┘    
doc      └───────┘  └┘   └──┘    
txt      └───────┘  └┘   └──┘    
par      └───────┘  └┘   └──┘    
pid      └───┘└──┘  └┘   └──┘    
st   ───────────────────────────────
977        0 < ∥(1:𝕜)∥ - ∥-h∥ : by rwa [norm_neg, sub_pos, ← dist_zero_right h, normed_field.norm_one]
id                                    └──────┘  └─────┘    └─────────────┘   └───────────────────┘
src  ───────┘   └┘       └─┘  └───┘└──────┘└┘└─────┘└──┘└─────────────┘ └┘└───────────────────┘└─
typ  ───────┘   └┘     └─┘  └───┘└──────┘└┘└─────┘└──┘└─────────────┘└┘└───────────────────┘└─
doc  ───────┘   └┘       └─┘  └───┘        └┘       └──┘                └┘                     └─
txt  ───────┘   └┘       └─┘  └───┘        └┘       └──┘                └┘                     └─
par  ───────┘   └┘       └─┘  └───┘        └┘       └──┘                └┘                     └─
pid  ───────┘   └┘       └─┘  └────┘        └┘       └──┘                └┘                     └─
st   ────────────────────────────┘└────────────┘└───────┘└───────────────────┘└─────────────────────┘
978        ... ≤ ∥1 - -h∥ : norm_sub_norm_le _ _
id                        └──────────────┘
src  ─────┘└──┘  └┘  └─┘└──────────────┘└────
typ  ─────┘└──┘  └┘  └─┘└──────────────┘└────
doc  ─────┘└──┘  └┘    └─┘                └────
txt  ─────┘└──┘  └┘    └─┘                └────
par  ─────┘└──┘  └┘    └─┘                └────
pid  ─────────┘  └┘    └─┘                └────
st   ─────┘└─────────────────────────────────────
979        ... = ∥1 + h∥ : by simp,
src  ─────────┘  └┘   └─┘  └──┘
typ  ─────────┘  └┘   └─┘  └──┘
doc  ─────────┘  └┘   └─┘  └──┘
txt  ─────────┘  └┘   └─┘  └──┘
par  ─────────┘  └┘   └─┘  └──┘
pid  ─────────┘  └┘   └─┘  └───┘
st   ───────────────────────┘└───┘└─
980      have : 1 + h ≠ 0 := (norm_pos_iff (1 + h)).mp this,
id                          └──────────┘            └──┘
src      └───────┘  └────┘ └──────────┘ └┘  └────┘
typ      └───────┘ └────┘ └──────────┘ └┘ └────┘└──┘
doc      └───────┘   └────┘              └┘  └────┘
txt      └───────┘   └────┘              └┘  └────┘
par      └───────┘   └────┘              └┘  └────┘
pid      └───┘└──┘   └───┘              └┘  └────┘
st   ─────────────────────────────────────────────────────┘└─
981      simp only [mem_set_of_eq, smul_eq_mul, inv_one],
id                  └───────────┘  └─────────┘  └─────┘
src      └─────────┘└───────────┘└┘└─────────┘└┘└─────┘
typ      └─────────┘└───────────┘└┘└─────────┘└┘└─────┘
doc      └─────────┘             └┘           └┘       
txt      └─────────┘             └┘           └┘       
par      └─────────┘             └┘           └┘       
pid          └──┘└┘             └┘           └┘       
st   ──────────────────────────────────────────────────┘└─
982      field_simp [this, -add_comm],
id                   └──┘
src      └──────────┘    └──────────┘
typ      └──────────┘└──┘└──────────┘
doc      └──────────┘    └──────────┘
txt      └──────────┘    └──────────┘
par      └──────────┘    └──────────┘
pid                    └──────────┘
st   ───────────────────────────────┘└─
983      ring },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
984    { exact univ_mem_sets' mul_one }
id             └────────────┘ └─────┘
src      └────┘└────────────┘└─────┘
typ      └────┘└────────────┘└─────┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ────────────────────────────────┘└─
985  end
st   ──┘
986  
987  theorem has_deriv_at_inv (x_ne_zero : x ≠ 0) :
id                                          
src                                          
typ                                         
988    has_deriv_at (λy, y⁻¹) (-(x^2)⁻¹) x :=
id     └──────────┘     └┘      └┘  
src    └──────────┘       └┘       └┘
typ    └──────────┘     └┘      └┘  
doc    └──────────┘
989  begin
st   └─────
990    have A : has_deriv_at (λy, y⁻¹) (-1) (x⁻¹ * x : 𝕜),
id              └──────────┘       └┘               
src    └───────┘└──────────┘  └─┘ └┘└┘ └─┘     └─┘ 
typ    └───────┘└──────────┘  └─┘ └┘└┘ └─┘    └─┘
doc    └───────┘└──────────┘  └─┘   └┘  └─┘      └─┘ 
txt    └───────┘              └─┘   └┘  └─┘      └─┘ 
par    └───────┘              └─┘   └┘  └─┘      └─┘ 
pid    └────┘└─┘              └─┘   └┘  └─┘      └─┘ 
st   ───────────────────────────────────────────────────┘
991      by { simp only [inv_mul_cancel x_ne_zero, has_deriv_at_inv_one] },
id                       └────────────┘ └───────┘  └──────────────────┘
src           └─────────┘└────────────┘         └┘└──────────────────┘└┘
typ           └─────────┘└────────────┘└───────┘└┘└──────────────────┘└┘
doc           └─────────┘                       └┘                    └┘
txt           └─────────┘                       └┘                    └┘
par           └─────────┘                       └┘                    └┘
pid               └──┘└┘                       └┘                    
st          └──────────────────────────────────────────────────────────┘└┘
992    have B : has_deriv_at (λy, x⁻¹ * y) (x⁻¹) x,
id              └──────────┘                     
src    └───────┘└──────────┘  └─┘     └┘    └┘
typ    └───────┘└──────────┘  └─┘     └┘    └┘
doc    └───────┘└──────────┘  └─┘     └┘    └┘
txt    └───────┘              └─┘     └┘    └┘
par    └───────┘              └─┘     └┘    └┘
pid    └────┘└─┘              └─┘     └┘    └┘
st   ────────────────────────────────────────────┘
993      by simpa only [mul_one] using (has_deriv_at_id x).const_mul x⁻¹,
id                      └─────┘         └─────────────┘              
src         └──────────┘└─────┘└──────┘ └─────────────┘ └──────────┘
typ         └──────────┘└─────┘└──────┘ └─────────────┘ └──────────┘
doc         └──────────┘       └──────┘                 └──────────┘
txt         └──────────┘       └──────┘                 └──────────┘
par         └──────────┘       └──────┘                 └──────────┘
pid              └──┘└┘       └────┘                 └──────────┘
st                                                                      └─
994    convert (A.comp x B : _).const_mul x⁻¹,
id              └────┘                   
src    └──────┘ └────┘  └──────────────┘
typ    └──────┘ └────┘ └──────────────┘
doc    └──────┘ └────┘  └──────────────┘
txt    └──────┘         └──────────────┘
par    └──────┘         └──────────────┘
pid                    └──────────────┘
st   ───────────────────────────────────────┘└─
995    { ext y,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
996      rw [function.comp_apply, mul_inv', inv_inv', mul_comm, mul_assoc, mul_inv_cancel x_ne_zero,
id           └─────────────────┘  └──────┘  └──────┘  └──────┘  └───────┘  └────────────┘ └───────┘
src      └──┘└─────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└────────────┘         └─
typ      └──┘└─────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└────────────┘└───────┘└─
doc      └──┘                   └┘        └┘        └┘        └┘         └┘                       └─
txt      └──┘                   └┘        └┘        └┘        └┘         └┘                       └─
par      └──┘                   └┘        └┘        └┘        └┘         └┘                       └─
pid        └┘                   └┘        └┘        └┘        └┘         └┘                       └─
st   ──────────────────────────┘└────────┘└────────┘└────────┘└─────────┘└────────────────────────┘└─
997        mul_one] },
id         └─────┘
src  ─────┘└─────┘└┘
typ  ─────┘└─────┘└┘
doc  ─────┘       └┘
txt  ─────┘       └┘
par  ─────┘       └┘
pid  ─────┘       
st   ────────────┘└┘
998    { rw [pow_two, mul_inv', smul_eq_mul, mul_neg_one, neg_mul_eq_mul_neg] }
id           └─────┘  └──────┘  └─────────┘  └─────────┘  └────────────────┘
src      └──┘└─────┘└┘└──────┘└┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
typ      └──┘└─────┘└┘└──────┘└┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
doc      └──┘       └┘        └┘           └┘└─────────┘└┘                  └┘
txt      └──┘       └┘        └┘           └┘           └┘                  └┘
par      └──┘       └┘        └┘           └┘           └┘                  └┘
pid        └┘       └┘        └┘           └┘           └┘                  
st   ──────────────┘└────────┘└───────────┘└───────────┘└──────────────────┘└─
999  end
st   ──┘
1000  
1001  theorem has_deriv_within_at_inv (x_ne_zero : x ≠ 0) (s : set 𝕜) :
id                                                          └─┘ 
src                                                          └─┘
typ                                                         └─┘ 
1002    has_deriv_within_at (λx, x⁻¹) (-(x^2)⁻¹) s x :=
id     └─────────────────┘     └┘      └┘   
src    └─────────────────┘       └┘       └┘
typ    └─────────────────┘     └┘      └┘   
doc    └─────────────────┘
1003  (has_deriv_at_inv x_ne_zero).has_deriv_within_at
id    └──────────────┘ └───────┘ └─────────────────┘
src   └──────────────┘           └─────────────────┘
typ   └──────────────┘ └───────┘ └─────────────────┘
1004  
1005  lemma differentiable_at_inv (x_ne_zero : x ≠ 0) :
id                                             
src                                             
typ                                            
1006    differentiable_at 𝕜 (λx, x⁻¹) x :=
id     └───────────────┘      └┘  
src    └───────────────┘         └┘
typ    └───────────────┘      └┘  
doc    └───────────────┘
1007  (has_deriv_at_inv x_ne_zero).differentiable_at
id    └──────────────┘ └───────┘ └───────────────┘
src   └──────────────┘           └───────────────┘
typ   └──────────────┘ └───────┘ └───────────────┘
1008  
1009  lemma differentiable_within_at_inv (x_ne_zero : x ≠ 0) :
id                                                    
src                                                    
typ                                                   
1010    differentiable_within_at 𝕜 (λx, x⁻¹) s x :=
id     └──────────────────────┘      └┘   
src    └──────────────────────┘         └┘
typ    └──────────────────────┘      └┘   
doc    └──────────────────────┘
1011  (differentiable_at_inv x_ne_zero).differentiable_within_at
id    └───────────────────┘ └───────┘ └──────────────────────┘
src   └───────────────────┘           └──────────────────────┘
typ   └───────────────────┘ └───────┘ └──────────────────────┘
1012  
1013  lemma differentiable_on_inv : differentiable_on 𝕜 (λx:𝕜, x⁻¹) {x | x ≠ 0} :=
id                                 └───────────────┘        └┘      
src                                └───────────────┘           └┘        
typ                                └───────────────┘        └┘      
doc                                └───────────────┘
1014  λx hx, differentiable_within_at_inv hx
id     └┘  └──────────────────────────┘ └┘
src         └──────────────────────────┘
typ    └┘  └──────────────────────────┘ └┘
1015  
1016  lemma deriv_inv (x_ne_zero : x ≠ 0) :
id                                 
src                                 
typ                                
1017    deriv (λx, x⁻¹) x = -(x^2)⁻¹ :=
id     └───┘     └┘       └┘
src    └───┘       └┘         └┘
typ    └───┘     └┘       └┘
doc    └───┘
1018  (has_deriv_at_inv x_ne_zero).deriv
id    └──────────────┘ └───────┘ └───┘
src   └──────────────┘           └───┘
typ   └──────────────┘ └───────┘ └───┘
1019  
1020  lemma deriv_within_inv (x_ne_zero : x ≠ 0) (hxs : unique_diff_within_at 𝕜 s x) :
id                                                   └───────────────────┘   
src                                                   └───────────────────┘
typ                                                  └───────────────────┘   
doc                                                    └───────────────────┘
1021    deriv_within (λx, x⁻¹) s x = -(x^2)⁻¹ :=
id     └──────────┘     └┘        └┘
src    └──────────┘       └┘           └┘
typ    └──────────┘     └┘        └┘
doc    └──────────┘
1022  begin
st   └─────
1023    rw differentiable_at.deriv_within (differentiable_at_inv x_ne_zero) hxs,
id        └────────────────────────────┘  └───────────────────┘ └───────┘  └─┘
src    └─┘└────────────────────────────┘ └───────────────────┘         └┘
typ    └─┘└────────────────────────────┘ └───────────────────┘└───────┘└┘└─┘
doc    └─┘                                                             └┘
txt    └─┘                                                             └┘
par    └─┘                                                             └┘
pid                                                                   └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
1024    exact deriv_inv x_ne_zero
id           └───────┘ └───────┘
src    └────┘└───────┘         
typ    └────┘└───────┘└───────┘
doc    └────┘                  
txt    └────┘                  
par    └────┘                  
pid                           
st   ───────────────────────────┘
1025  end
st   └─┘
1026  
1027  lemma has_fderiv_at_inv (x_ne_zero : x ≠ 0) :
id                                         
src                                         
typ                                        
1028    has_fderiv_at (λx, x⁻¹) (smul_right 1 (-(x^2)⁻¹) : 𝕜 →L[𝕜] 𝕜) x :=
id     └───────────┘     └┘   └────────┘       └┘     └─┘   
src    └───────────┘       └┘   └────────┘        └┘      └─┘ 
typ    └───────────┘     └┘   └────────┘       └┘     └─┘   
doc    └───────────┘            └────────┘                  └─┘ 
1029  has_deriv_at_inv x_ne_zero
id   └──────────────┘ └───────┘
src  └──────────────┘
typ  └──────────────┘ └───────┘
1030  
1031  lemma has_fderiv_within_at_inv (x_ne_zero : x ≠ 0) :
id                                                
src                                                
typ                                               
1032    has_fderiv_within_at (λx, x⁻¹) (smul_right 1 (-(x^2)⁻¹) : 𝕜 →L[𝕜] 𝕜) s x :=
id     └──────────────────┘     └┘   └────────┘       └┘     └─┘    
src    └──────────────────┘       └┘   └────────┘        └┘      └─┘ 
typ    └──────────────────┘     └┘   └────────┘       └┘     └─┘    
doc    └──────────────────┘            └────────┘                  └─┘ 
1033  (has_fderiv_at_inv x_ne_zero).has_fderiv_within_at
id    └───────────────┘ └───────┘ └──────────────────┘
src   └───────────────┘           └──────────────────┘
typ   └───────────────┘ └───────┘ └──────────────────┘
1034  
1035  lemma fderiv_inv (x_ne_zero : x ≠ 0) :
id                                  
src                                  
typ                                 
1036    fderiv 𝕜 (λx, x⁻¹) x = smul_right 1 (-(x^2)⁻¹) :=
id     └────┘      └┘    └────────┘       └┘
src    └────┘         └┘     └────────┘        └┘
typ    └────┘      └┘    └────────┘       └┘
doc    └────┘                 └────────┘
1037  (has_fderiv_at_inv x_ne_zero).fderiv
id    └───────────────┘ └───────┘ └────┘
src   └───────────────┘           └────┘
typ   └───────────────┘ └───────┘ └────┘
1038  
1039  lemma fderiv_within_inv (x_ne_zero : x ≠ 0) (hxs : unique_diff_within_at 𝕜 s x) :
id                                                    └───────────────────┘   
src                                                    └───────────────────┘
typ                                                   └───────────────────┘   
doc                                                     └───────────────────┘
1040    fderiv_within 𝕜 (λx, x⁻¹) s x = smul_right 1 (-(x^2)⁻¹) :=
id     └───────────┘      └┘     └────────┘       └┘
src    └───────────┘         └┘       └────────┘        └┘
typ    └───────────┘      └┘     └────────┘       └┘
doc    └───────────┘                   └────────┘
1041  begin
st   └─────
1042    rw differentiable_at.fderiv_within (differentiable_at_inv x_ne_zero) hxs,
id        └─────────────────────────────┘  └───────────────────┘ └───────┘  └─┘
src    └─┘└─────────────────────────────┘ └───────────────────┘         └┘
typ    └─┘└─────────────────────────────┘ └───────────────────┘└───────┘└┘└─┘
doc    └─┘                                                              └┘
txt    └─┘                                                              └┘
par    └─┘                                                              └┘
pid                                                                    └┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
1043    exact fderiv_inv x_ne_zero
id           └────────┘ └───────┘
src    └────┘└────────┘         
typ    └────┘└────────┘└───────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ────────────────────────────┘
1044  end
st   └─┘
1045  
1046  end inverse
1047  
1048  section division
1049  /-! ### Derivative of `x ↦ c x / d x` -/
1050  
1051  variables {c d : 𝕜 → 𝕜} {c' d' : 𝕜}
1052  
1053  lemma has_deriv_within_at.div
1054    (hc : has_deriv_within_at c c' s x) (hd : has_deriv_within_at d d' s x) (hx : d x ≠ 0) :
id           └─────────────────┘  └┘          └─────────────────┘  └┘            
src          └─────────────────┘                 └─────────────────┘                     
typ          └─────────────────┘  └┘          └─────────────────┘  └┘            
doc          └─────────────────┘                 └─────────────────┘
1055    has_deriv_within_at (λ y, c y / d y) ((c' * d x - c x * d') / (d x)^2) s x :=
id     └─────────────────┘              └┘        └┘          
src    └─────────────────┘                                           
typ    └─────────────────┘              └┘        └┘          
doc    └─────────────────┘
1056  begin
st   └─────
1057    have A : (d x)⁻¹ * (d x)⁻¹ * (c' * d x) = (d x)⁻¹ * c',
id                   └┘                                └┘
src    └───────┘   └┘            └┘      
typ    └───────┘   └┘            └┘    └┘
doc    └───────┘                  └┘       
txt    └───────┘                  └┘       
par    └───────┘                  └┘       
pid    └────┘└─┘                  └┘       
st   ───────────────────────────────────────────────────────┘
1058      by rw [← mul_assoc, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel hx, one_mul],
id                └───────┘  └──────┘    └───────┘    └───────┘  └────────────┘ └┘  └─────┘
src         └────┘└───────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘  └┘└─────┘
typ         └────┘└───────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘└┘└┘└─────┘
doc         └────┘         └┘        └──┘         └──┘         └┘                └┘       
txt         └────┘         └┘        └──┘         └──┘         └┘                └┘       
par         └────┘         └┘        └──┘         └──┘         └┘                └┘       
pid           └──┘         └┘        └──┘         └──┘         └┘                └┘       
st              └─────────┘└────────┘└───────────┘└───────────┘└─────────────────┘└───────┘└─
1059    convert hc.mul ((has_deriv_at_inv hx).comp_has_deriv_within_at x hd),
id             └────┘   └──────────────┘ └┘                            └┘
src    └──────┘└────┘  └──────────────┘  └─────────────────────────┘   
typ    └──────┘└────┘  └──────────────┘└┘└─────────────────────────┘└┘
doc    └──────┘                          └─────────────────────────┘   
txt    └──────┘                          └─────────────────────────┘   
par    └──────┘                          └─────────────────────────┘   
pid                                     └─────────────────────────┘   
st   ─────────────────────────────────────────────────────────────────────┘└─
1060    simp [div_eq_inv_mul, pow_two, mul_inv', mul_add, A],
id           └────────────┘  └─────┘  └──────┘  └─────┘  
src    └────┘└────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└┘ 
typ    └────┘└────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└┘
doc    └────┘              └┘       └┘        └┘       └┘ 
txt    └────┘              └┘       └┘        └┘       └┘ 
par    └────┘              └┘       └┘        └┘       └┘ 
pid                      └┘       └┘        └┘       └┘ 
st   ─────────────────────────────────────────────────────┘└─
1061    ring
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
1062  end
st   └─┘
1063  
1064  lemma has_deriv_at.div (hc : has_deriv_at c c' x) (hd : has_deriv_at d d' x) (hx : d x ≠ 0) :
id                                └──────────┘  └┘         └──────────┘  └┘           
src                               └──────────┘               └──────────┘                   
typ                               └──────────┘  └┘         └──────────┘  └┘           
doc                               └──────────┘               └──────────┘
1065    has_deriv_at (λ y, c y / d y) ((c' * d x - c x * d') / (d x)^2) x :=
id     └──────────┘              └┘        └┘         
src    └──────────┘                                           
typ    └──────────┘              └┘        └┘         
doc    └──────────┘
1066  begin
st   └─────
1067    rw ← has_deriv_within_at_univ at *,
id          └──────────────────────┘
src    └───┘└──────────────────────┘└───┘
typ    └───┘└──────────────────────┘└───┘
doc    └───┘                        └───┘
txt    └───┘                        └───┘
par    └───┘                        └───┘
pid      └─┘                        └───┘
st   ───────────────────────────────────┘└─
1068    exact hc.div hd hx
id           └────┘ └┘ └┘
src    └────┘└────┘    
typ    └────┘└────┘└┘└┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                   
st   ────────────────────┘
1069  end
st   └─┘
1070  
1071  lemma differentiable_within_at.div
1072    (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) (hx : d x ≠ 0) :
id           └──────────────────────┘            └──────────────────────┘              
src          └──────────────────────┘                └──────────────────────┘                    
typ          └──────────────────────┘            └──────────────────────┘              
doc          └──────────────────────┘                └──────────────────────┘
1073  differentiable_within_at 𝕜 (λx, c x / d x) s x :=
id   └──────────────────────┘             
src  └──────────────────────┘            
typ  └──────────────────────┘             
doc  └──────────────────────┘
1074  ((hc.has_deriv_within_at).div (hd.has_deriv_within_at) hx).differentiable_within_at
id     └┘└──────────────────┘ └─┘   └┘└──────────────────┘  └┘ └──────────────────────┘
src      └──────────────────┘ └─┘     └──────────────────┘     └──────────────────────┘
typ    └┘└──────────────────┘ └─┘   └┘└──────────────────┘  └┘ └──────────────────────┘
1075  
1076  lemma differentiable_at.div
1077    (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜 d x) (hx : d x ≠ 0) :
id           └───────────────┘           └───────────────┘             
src          └───────────────┘              └───────────────┘                  
typ          └───────────────┘           └───────────────┘             
doc          └───────────────┘              └───────────────┘
1078  differentiable_at 𝕜 (λx, c x / d x) x :=
id   └───────────────┘            
src  └───────────────┘            
typ  └───────────────┘            
doc  └───────────────┘
1079  ((hc.has_deriv_at).div (hd.has_deriv_at) hx).differentiable_at
id     └┘└───────────┘ └─┘   └┘└───────────┘  └┘ └───────────────┘
src      └───────────┘ └─┘     └───────────┘     └───────────────┘
typ    └┘└───────────┘ └─┘   └┘└───────────┘  └┘ └───────────────┘
1080  
1081  lemma differentiable_on.div
1082    (hc : differentiable_on 𝕜 c s) (hd : differentiable_on 𝕜 d s) (hx : ∀ x ∈ s, d x ≠ 0) :
id           └───────────────┘           └───────────────┘                    
src          └───────────────┘              └───────────────┘                           
typ          └───────────────┘           └───────────────┘                    
doc          └───────────────┘              └───────────────┘
1083  differentiable_on 𝕜 (λx, c x / d x) s :=
id   └───────────────┘            
src  └───────────────┘            
typ  └───────────────┘            
doc  └───────────────┘
1084  λx h, (hc x h).div (hd x h) (hx x h)
id        └┘   └─┘   └┘     └┘  
src                └─┘
typ       └┘   └─┘   └┘     └┘  
1085  
1086  lemma differentiable.div
1087    (hc : differentiable 𝕜 c) (hd : differentiable 𝕜 d) (hx : ∀ x, d x ≠ 0) :
id           └────────────┘          └────────────┘                
src          └────────────┘            └────────────┘                     
typ          └────────────┘          └────────────┘                
doc          └────────────┘            └────────────┘
1088  differentiable 𝕜 (λx, c x / d x) :=
id   └────────────┘          
src  └────────────┘            
typ  └────────────┘          
doc  └────────────┘
1089  λx, (hc x).div (hd x) (hx x)
id       └┘  └─┘   └┘    └┘ 
src            └─┘
typ      └┘  └─┘   └┘    └┘ 
1090  
1091  lemma deriv_within_div
1092    (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) (hx : d x ≠ 0)
id           └──────────────────────┘            └──────────────────────┘              
src          └──────────────────────┘                └──────────────────────┘                    
typ          └──────────────────────┘            └──────────────────────┘              
doc          └──────────────────────┘                └──────────────────────┘
1093    (hxs : unique_diff_within_at 𝕜 s x) :
id            └───────────────────┘   
src           └───────────────────┘
typ           └───────────────────┘   
doc           └───────────────────┘
1094    deriv_within (λx, c x / d x) s x
id     └──────────┘            
src    └──────────┘          
typ    └──────────┘            
doc    └──────────┘
1095      = ((deriv_within c s x) * d x - c x * (deriv_within d s x)) / (d x)^2 :=
id          └──────────┘             └──────────┘          
src         └──────────┘                    └──────────┘               
typ         └──────────┘             └──────────┘          
doc          └──────────┘                       └──────────┘
1096  ((hc.has_deriv_within_at).div (hd.has_deriv_within_at) hx).deriv_within hxs
id     └┘└──────────────────┘ └─┘   └┘└──────────────────┘  └┘ └──────────┘  └─┘
src      └──────────────────┘ └─┘     └──────────────────┘     └──────────┘
typ    └┘└──────────────────┘ └─┘   └┘└──────────────────┘  └┘ └──────────┘  └─┘
1097  
1098  lemma deriv_div
1099    (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜 d x) (hx : d x ≠ 0) :
id           └───────────────┘           └───────────────┘             
src          └───────────────┘              └───────────────┘                  
typ          └───────────────┘           └───────────────┘             
doc          └───────────────┘              └───────────────┘
1100    deriv (λx, c x / d x) x = ((deriv c x) * d x - c x * (deriv d x)) / (d x)^2 :=
id     └───┘               └───┘            └───┘         
src    └───┘                     └───┘                  └───┘             
typ    └───┘               └───┘            └───┘         
doc    └───┘                       └───┘                     └───┘
1101  ((hc.has_deriv_at).div (hd.has_deriv_at) hx).deriv
id     └┘└───────────┘ └─┘   └┘└───────────┘  └┘ └───┘
src      └───────────┘ └─┘     └───────────┘     └───┘
typ    └┘└───────────┘ └─┘   └┘└───────────┘  └┘ └───┘
1102  
1103  end division
1104  end
1105  
1106  namespace polynomial
1107  /-! ### Derivative of a polynomial -/
1108  
1109  variables {x : 𝕜} {s : set 𝕜}
id                          └─┘
src                         └─┘
typ                         └─┘
1110  variable (p : polynomial 𝕜)
id                 └────────┘
src                └────────┘
typ                └────────┘
doc                └────────┘
1111  
1112  /-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`. -/
1113  protected lemma has_deriv_at (x : 𝕜) : has_deriv_at (λx, p.eval x) (p.derivative.eval x) x :=
id                                         └──────────┘     └───┘    └─────────┘└───┘   
src                                         └──────────┘       └───┘      └─────────┘└───┘
typ                                        └──────────┘     └───┘    └─────────┘└───┘   
doc                                         └──────────┘       └───┘      └─────────┘└───┘
1114  begin
st   └─────
1115    apply p.induction_on,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────┘└─
1116    { simp [has_deriv_at_const] },
id             └────────────────┘
src      └────┘└────────────────┘└┘
typ      └────┘└────────────────┘└┘
doc      └────┘                  └┘
txt      └────┘                  └┘
par      └────┘                  └┘
pid                            
st   ───┘└────────────────────────┘└┘
1117    { assume p q hp hq,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid      └──────────────┘
st   ───┘└──────────────┘└─
1118      convert hp.add hq;
id               └────┘ └┘
src      └──────┘└────┘
typ      └──────┘└────┘└┘
doc      └──────┘      
txt      └──────┘      
par      └──────┘      
pid                   
st   ───────────────────────
1119      simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
1120    { assume n a h,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
1121      convert h.mul (has_deriv_at_id x),
id               └───┘  └─────────────┘ 
src      └──────┘└───┘ └─────────────┘ 
typ      └──────┘└───┘ └─────────────┘
doc      └──────┘                      
txt      └──────┘                      
par      └──────┘                      
pid                                   
st   ────────────────────────────────────┘└─
1122      { ext y, simp [pow_add, mul_assoc] },
id                      └─────┘  └───────┘
src        └───┘  └────┘└─────┘└┘└───────┘└┘
typ        └───┘  └────┘└─────┘└┘└───────┘└┘
doc        └───┘  └────┘       └┘         └┘
txt        └───┘  └────┘       └┘         └┘
par        └───┘  └────┘       └┘         └┘
pid           └┘             └┘         
st   ─────┘└───┘└──────────────────────────┘└┘
1123      { simp [pow_add], ring } }
id               └─────┘
src        └────┘└─────┘  └───┘
typ        └────┘└─────┘  └───┘
doc        └────┘         └───┘
txt        └────┘         └───┘
par        └────┘         └───┘
pid                         
st   ───────────────────┘└─────┘└───
1124  end
st   ──┘
1125  
1126  protected theorem has_deriv_within_at (x : 𝕜) (s : set 𝕜) :
id                                                     └─┘ 
src                                                     └─┘
typ                                                    └─┘ 
1127    has_deriv_within_at (λx, p.eval x) (p.derivative.eval x) s x :=
id     └─────────────────┘     └───┘    └─────────┘└───┘    
src    └─────────────────┘       └───┘      └─────────┘└───┘
typ    └─────────────────┘     └───┘    └─────────┘└───┘    
doc    └─────────────────┘       └───┘      └─────────┘└───┘
1128  (p.has_deriv_at x).has_deriv_within_at
id    └───────────┘  └─────────────────┘
src    └───────────┘   └─────────────────┘
typ   └───────────┘  └─────────────────┘
doc    └───────────┘
1129  
1130  protected lemma differentiable_at : differentiable_at 𝕜 (λx, p.eval x) x :=
id                                       └───────────────┘      └───┘   
src                                      └───────────────┘         └───┘
typ                                      └───────────────┘      └───┘   
doc                                      └───────────────┘         └───┘
1131  (p.has_deriv_at x).differentiable_at
id    └───────────┘  └───────────────┘
src    └───────────┘   └───────────────┘
typ   └───────────┘  └───────────────┘
doc    └───────────┘
1132  
1133  protected lemma differentiable_within_at : differentiable_within_at 𝕜 (λx, p.eval x) s x :=
id                                              └──────────────────────┘      └───┘    
src                                             └──────────────────────┘         └───┘
typ                                             └──────────────────────┘      └───┘    
doc                                             └──────────────────────┘         └───┘
1134  p.differentiable_at.differentiable_within_at
id   └────────────────┘└───────────────────────┘
src   └────────────────┘└───────────────────────┘
typ  └────────────────┘└───────────────────────┘
1135  
1136  protected lemma differentiable : differentiable 𝕜 (λx, p.eval x) :=
id                                    └────────────┘      └───┘ 
src                                   └────────────┘         └───┘
typ                                   └────────────┘      └───┘ 
doc                                   └────────────┘         └───┘
1137  λx, p.differentiable_at
id      └────────────────┘
src       └────────────────┘
typ     └────────────────┘
1138  
1139  protected lemma differentiable_on : differentiable_on 𝕜 (λx, p.eval x) s :=
id                                       └───────────────┘      └───┘   
src                                      └───────────────┘         └───┘
typ                                      └───────────────┘      └───┘   
doc                                      └───────────────┘         └───┘
1140  p.differentiable.differentiable_on
id   └─────────────┘└────────────────┘
src   └─────────────┘└────────────────┘
typ  └─────────────┘└────────────────┘
1141  
1142  @[simp] protected lemma deriv : deriv (λx, p.eval x) x = p.derivative.eval x :=
id                                   └───┘     └───┘     └─────────┘└───┘ 
src                                  └───┘       └───┘        └─────────┘└───┘
typ                                  └───┘     └───┘     └─────────┘└───┘ 
doc    └──┘                          └───┘       └───┘         └─────────┘└───┘
1143  (p.has_deriv_at x).deriv
id    └───────────┘  └───┘
src    └───────────┘   └───┘
typ   └───────────┘  └───┘
doc    └───────────┘
1144  
1145  protected lemma deriv_within (hxs : unique_diff_within_at 𝕜 s x) :
id                                       └───────────────────┘   
src                                      └───────────────────┘
typ                                      └───────────────────┘   
doc                                      └───────────────────┘
1146    deriv_within (λx, p.eval x) s x = p.derivative.eval x :=
id     └──────────┘     └───┘      └─────────┘└───┘ 
src    └──────────┘       └───┘          └─────────┘└───┘
typ    └──────────┘     └───┘      └─────────┘└───┘ 
doc    └──────────┘       └───┘           └─────────┘└───┘
1147  begin
st   └─────
1148    rw differentiable_at.deriv_within p.differentiable_at hxs,
id        └────────────────────────────┘ └─────────────────┘ └─┘
src    └─┘└────────────────────────────┘└─────────────────┘
typ    └─┘└────────────────────────────┘└─────────────────┘└─┘
doc    └─┘                                                 
txt    └─┘                                                 
par    └─┘                                                 
pid                                                       
st   ──────────────────────────────────────────────────────────┘└─
1149    exact p.deriv
id           └─────┘
src    └────┘└─────┘
typ    └────┘└─────┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid                
st   ───────────────┘
1150  end
st   └─┘
1151  
1152  protected lemma continuous : continuous (λx, p.eval x) :=
id                                └────────┘     └───┘ 
src                               └────────┘       └───┘
typ                               └────────┘     └───┘ 
doc                               └────────┘       └───┘
1153  p.differentiable.continuous
id   └─────────────┘└─────────┘
src   └─────────────┘└─────────┘
typ  └─────────────┘└─────────┘
1154  
1155  protected lemma continuous_on : continuous_on (λx, p.eval x) s :=
id                                   └───────────┘     └───┘   
src                                  └───────────┘       └───┘
typ                                  └───────────┘     └───┘   
doc                                  └───────────┘       └───┘
1156  p.continuous.continuous_on
id   └─────────┘└────────────┘
src   └─────────┘└────────────┘
typ  └─────────┘└────────────┘
1157  
1158  protected lemma continuous_at : continuous_at (λx, p.eval x) x :=
id                                   └───────────┘     └───┘   
src                                  └───────────┘       └───┘
typ                                  └───────────┘     └───┘   
doc                                  └───────────┘       └───┘
1159  p.continuous.continuous_at
id   └─────────┘└────────────┘
src   └─────────┘└────────────┘
typ  └─────────┘└────────────┘
1160  
1161  protected lemma continuous_within_at : continuous_within_at (λx, p.eval x) s x :=
id                                          └──────────────────┘     └───┘    
src                                         └──────────────────┘       └───┘
typ                                         └──────────────────┘     └───┘    
doc                                         └──────────────────┘       └───┘
1162  p.continuous_at.continuous_within_at
id   └────────────┘└───────────────────┘
src   └────────────┘└───────────────────┘
typ  └────────────┘└───────────────────┘
1163  
1164  protected lemma has_fderiv_at (x : 𝕜) :
id                                      
typ                                     
1165    has_fderiv_at (λx, p.eval x) (smul_right 1 (p.derivative.eval x) : 𝕜 →L[𝕜] 𝕜) x :=
id     └───────────┘     └───┘    └────────┘    └─────────┘└───┘      └─┘   
src    └───────────┘       └───┘     └────────┘     └─────────┘└───┘        └─┘ 
typ    └───────────┘     └───┘    └────────┘    └─────────┘└───┘      └─┘   
doc    └───────────┘       └───┘     └────────┘     └─────────┘└───┘        └─┘ 
1166  by simpa [has_deriv_at_iff_has_fderiv_at] using p.has_deriv_at x
id             └────────────────────────────┘        └────────────┘ 
src     └─────┘└────────────────────────────┘└──────┘└────────────┘ 
typ     └─────┘└────────────────────────────┘└──────┘└────────────┘
doc     └─────┘└────────────────────────────┘└──────┘└────────────┘ 
txt     └─────┘                              └──────┘               
par     └─────┘                              └──────┘               
pid                                        └────┘               
st     └──────────────────────────────────────────────────────────────
1167  
src  
typ  
doc  
txt  
par  
pid  
st   
1168  protected lemma has_fderiv_within_at (x : 𝕜) :
id                                             
typ                                            
1169    has_fderiv_within_at (λx, p.eval x) (smul_right 1 (p.derivative.eval x) : 𝕜 →L[𝕜] 𝕜) s x :=
id     └──────────────────┘     └───┘    └────────┘    └─────────┘└───┘      └─┘    
src    └──────────────────┘       └───┘     └────────┘     └─────────┘└───┘        └─┘ 
typ    └──────────────────┘     └───┘    └────────┘    └─────────┘└───┘      └─┘    
doc    └──────────────────┘       └───┘     └────────┘     └─────────┘└───┘        └─┘ 
1170  (p.has_fderiv_at x).has_fderiv_within_at
id    └────────────┘  └──────────────────┘
src    └────────────┘   └──────────────────┘
typ   └────────────┘  └──────────────────┘
1171  
1172  @[simp] protected lemma fderiv : fderiv 𝕜 (λx, p.eval x) x = smul_right 1 (p.derivative.eval x) :=
id                                    └────┘      └───┘     └────────┘    └─────────┘└───┘ 
src                                   └────┘         └───┘       └────────┘     └─────────┘└───┘
typ                                   └────┘      └───┘     └────────┘    └─────────┘└───┘ 
doc    └──┘                           └────┘         └───┘        └────────┘     └─────────┘└───┘
1173  (p.has_fderiv_at x).fderiv
id    └────────────┘  └────┘
src    └────────────┘   └────┘
typ   └────────────┘  └────┘
1174  
1175  protected lemma fderiv_within (hxs : unique_diff_within_at 𝕜 s x) :
id                                        └───────────────────┘   
src                                       └───────────────────┘
typ                                       └───────────────────┘   
doc                                       └───────────────────┘
1176    fderiv_within 𝕜 (λx, p.eval x) s x = smul_right 1 (p.derivative.eval x) :=
id     └───────────┘      └───┘      └────────┘    └─────────┘└───┘ 
src    └───────────┘         └───┘         └────────┘     └─────────┘└───┘
typ    └───────────┘      └───┘      └────────┘    └─────────┘└───┘ 
doc    └───────────┘         └───┘          └────────┘     └─────────┘└───┘
1177  begin
st   └─────
1178    rw differentiable_at.fderiv_within p.differentiable_at hxs,
id        └─────────────────────────────┘ └─────────────────┘ └─┘
src    └─┘└─────────────────────────────┘└─────────────────┘
typ    └─┘└─────────────────────────────┘└─────────────────┘└─┘
doc    └─┘                                                  
txt    └─┘                                                  
par    └─┘                                                  
pid                                                        
st   ───────────────────────────────────────────────────────────┘└─
1179    exact p.fderiv
id           └──────┘
src    └────┘└──────┘
typ    └────┘└──────┘
doc    └────┘        
txt    └────┘        
par    └────┘        
pid                 
st   ────────────────┘
1180  end
st   └─┘
1181  
1182  end polynomial
1183  
1184  section pow
1185  /-! ### Derivative of `x ↦ x^n` for `n : ℕ` -/
1186  variables {x : 𝕜} {s : set 𝕜}
id                          └─┘
src                         └─┘
typ                         └─┘
1187  variable {n : ℕ }
id                 
src                
typ                
1188  
1189  lemma has_deriv_at_pow (n : ℕ) (x : 𝕜) : has_deriv_at (λx, x^n) ((n : 𝕜) * x^(n-1)) x :=
id                                          └──────────┘                    
src                                          └──────────┘                       
typ                                         └──────────┘                    
doc                                           └──────────┘
1190  begin
st   └─────
1191    convert (polynomial.C 1 * (polynomial.X)^n).has_deriv_at x,
id              └──────────┘     └──────────┘                
src    └──────┘ └──────────┘└─┘ └──────────┘ └─────────────┘
typ    └──────┘ └──────────┘└─┘ └──────────┘└─────────────┘
doc    └──────┘ └──────────┘└─┘  └──────────┘  └─────────────┘
txt    └──────┘             └─┘                └─────────────┘
par    └──────┘             └─┘                └─────────────┘
pid                        └─┘                └─────────────┘
st   ───────────────────────────────────────────────────────────┘└─
1192    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
1193    { rw [polynomial.derivative_monomial], simp }
id           └────────────────────────────┘
src      └──┘└────────────────────────────┘  └───┘
typ      └──┘└────────────────────────────┘  └───┘
doc      └──┘                                └───┘
txt      └──┘                                └───┘
par      └──┘                                └───┘
pid        └┘                                    
st   ─────────────────────────────────────┘└──────┘└─
1194  end
st   ──┘
1195  
1196  theorem has_deriv_within_at_pow (n : ℕ) (x : 𝕜) (s : set 𝕜) :
id                                                      └─┘ 
src                                                      └─┘
typ                                                     └─┘ 
1197    has_deriv_within_at (λx, x^n) ((n : 𝕜) * x^(n-1)) s x :=
id     └─────────────────┘                     
src    └─────────────────┘                       
typ    └─────────────────┘                     
doc    └─────────────────┘
1198  (has_deriv_at_pow n x).has_deriv_within_at
id    └──────────────┘   └─────────────────┘
src   └──────────────┘     └─────────────────┘
typ   └──────────────┘   └─────────────────┘
1199  
1200  lemma differentiable_at_pow : differentiable_at 𝕜 (λx, x^n) x :=
id                                 └───────────────┘        
src                                └───────────────┘         
typ                                └───────────────┘        
doc                                └───────────────┘
1201  (has_deriv_at_pow n x).differentiable_at
id    └──────────────┘   └───────────────┘
src   └──────────────┘     └───────────────┘
typ   └──────────────┘   └───────────────┘
1202  
1203  lemma differentiable_within_at_pow : differentiable_within_at 𝕜 (λx, x^n) s x :=
id                                        └──────────────────────┘         
src                                       └──────────────────────┘         
typ                                       └──────────────────────┘         
doc                                       └──────────────────────┘
1204  differentiable_at_pow.differentiable_within_at
id   └───────────────────┘└───────────────────────┘
src  └───────────────────┘└───────────────────────┘
typ  └───────────────────┘└───────────────────────┘
1205  
1206  lemma differentiable_pow : differentiable 𝕜 (λx:𝕜, x^n) :=
id                              └────────────┘        
src                             └────────────┘           
typ                             └────────────┘        
doc                             └────────────┘
1207  λx, differentiable_at_pow
id      └───────────────────┘
src      └───────────────────┘
typ     └───────────────────┘
1208  
1209  lemma differentiable_on_pow : differentiable_on 𝕜 (λx, x^n) s :=
id                                 └───────────────┘        
src                                └───────────────┘         
typ                                └───────────────┘        
doc                                └───────────────┘
1210  differentiable_pow.differentiable_on
id   └────────────────┘└────────────────┘
src  └────────────────┘└────────────────┘
typ  └────────────────┘└────────────────┘
1211  
1212  lemma deriv_pow : deriv (λx, x^n) x = (n : 𝕜) * x^(n-1) :=
id                     └───┘                 
src                    └───┘                         
typ                    └───┘                 
doc                    └───┘
1213  (has_deriv_at_pow n x).deriv
id    └──────────────┘   └───┘
src   └──────────────┘     └───┘
typ   └──────────────┘   └───┘
1214  
1215  @[simp] lemma deriv_pow' : deriv (λx, x^n) = λ x, (n : 𝕜) * x^(n-1) :=
id                              └───┘                    
src                             └───┘                            
typ                             └───┘                    
doc    └──┘                     └───┘
1216  funext $ λ x, deriv_pow
id   └────┘       └───────┘
src  └────┘        └───────┘
typ  └────┘       └───────┘
1217  
1218  lemma deriv_within_pow (hxs : unique_diff_within_at 𝕜 s x) :
id                                 └───────────────────┘   
src                                └───────────────────┘
typ                                └───────────────────┘   
doc                                └───────────────────┘
1219    deriv_within (λx, x^n) s x = (n : 𝕜) * x^(n-1) :=
id     └──────────┘                  
src    └──────────┘                           
typ    └──────────┘                  
doc    └──────────┘
1220  by rw [differentiable_at_pow.deriv_within hxs, deriv_pow]
id          └────────────────────────────────┘ └─┘  └───────┘
src     └──┘└────────────────────────────────┘   └┘└───────┘└─
typ     └──┘└────────────────────────────────┘└─┘└┘└───────┘└─
doc     └──┘                                     └┘         └─
txt     └──┘                                     └┘         └─
par     └──┘                                     └┘         └─
pid       └┘                                     └┘         
st     └─────────────────────────────────────────┘└─────────┘
1221  
src  
typ  
doc  
txt  
par  
pid  
st   
1222  end pow
1223  
1224  /-! ### Upper estimates on liminf and limsup -/
1225  
1226  section real
1227  
1228  variables {f : ℝ → ℝ} {f' : ℝ} {s : set ℝ} {x : ℝ} {r : ℝ}
id                                    └─┘               
src                                   └─┘               
typ                                   └─┘               
1229  
1230  lemma has_deriv_within_at.limsup_slope_le (hf : has_deriv_within_at f f' s x) (hr : f' < r) :
id                                                   └─────────────────┘  └┘          └┘  
src                                                  └─────────────────┘                    
typ                                                  └─────────────────┘  └┘          └┘  
doc                                                  └─────────────────┘
1231    ∀ᶠ z in nhds_within x (s \ {x}), (z - x)⁻¹ * (f z - f x) < r :=
id     └┘  └┘ └─────────┘            └┘          
src    └┘   └┘ └─────────┘                 └┘             
typ    └┘  └┘ └─────────┘            └┘          
doc    └┘   └┘ └─────────┘            
1232  has_deriv_within_at_iff_tendsto_slope.1 hf (mem_nhds_sets is_open_Iio hr)
id   └───────────────────────────────────┘  └┘  └───────────┘ └─────────┘ └┘
src  └───────────────────────────────────┘      └───────────┘ └─────────┘
typ  └───────────────────────────────────┘  └┘  └───────────┘ └─────────┘ └┘
1233  
1234  lemma has_deriv_within_at.limsup_slope_le' (hf : has_deriv_within_at f f' s x)
id                                                    └─────────────────┘  └┘  
src                                                   └─────────────────┘
typ                                                   └─────────────────┘  └┘  
doc                                                   └─────────────────┘
1235    (hs : x ∉ s) (hr : f' < r) :
id                     └┘  
src                         
typ                    └┘  
1236    ∀ᶠ z in nhds_within x s, (z - x)⁻¹ * (f z - f x) < r :=
id     └┘  └┘ └─────────┘       └┘          
src    └┘   └┘ └─────────┘           └┘             
typ    └┘  └┘ └─────────┘       └┘          
doc    └┘   └┘ └─────────┘    
1237  (has_deriv_within_at_iff_tendsto_slope' hs).1 hf (mem_nhds_sets is_open_Iio hr)
id    └────────────────────────────────────┘ └┘   └┘  └───────────┘ └─────────┘ └┘
src   └────────────────────────────────────┘          └───────────┘ └─────────┘
typ   └────────────────────────────────────┘ └┘   └┘  └───────────┘ └─────────┘ └┘
1238  
1239  lemma has_deriv_within_at.liminf_right_slope_le
1240    (hf : has_deriv_within_at f f' (Ioi x) x) (hr : f' < r) :
id           └─────────────────┘  └┘  └─┘           └┘  
src          └─────────────────┘       └─┘                
typ          └─────────────────┘  └┘  └─┘           └┘  
doc          └─────────────────┘       └─┘
1241    ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r :=
id     └┘  └┘ └─────────┘   └─┘       └┘          
src    └┘   └┘ └─────────┘    └─┘          └┘             
typ    └┘  └┘ └─────────┘   └─┘       └┘          
doc    └┘   └┘ └─────────┘    └─┘   
1242  (hf.limsup_slope_le' (lt_irrefl x) hr).frequently (nhds_within_Ioi_self_ne_bot x)
id    └┘└───────────────┘  └───────┘   └┘ └────────┘   └─────────────────────────┘ 
src     └───────────────┘  └───────┘       └────────┘   └─────────────────────────┘
typ   └┘└───────────────┘  └───────┘   └┘ └────────┘   └─────────────────────────┘ 
1243  
1244  end real
1245  
1246  section real_space
1247  
1248  open metric
1249  
1250  variables {E : Type u} [normed_group E] [normed_space ℝ E] {f : ℝ → E} {f' : E} {s : set ℝ}
id                          └──────────┘     └──────────┘                              └─┘ 
src                          └──────────┘     └──────────┘                              └─┘ 
typ                         └──────────┘     └──────────┘                              └─┘ 
doc                          └──────────┘     └──────────┘
1251    {x r : ℝ}
id            
src           
typ           
1252  
1253  /-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ∥f'∥` the ratio
1254  `∥f z - f x∥ / ∥z - x∥` is less than `r` in some neighborhood of `x` within `s`.
1255  In other words, the limit superior of this ratio as `z` tends to `x` along `s`
1256  is less than or equal to `∥f'∥`. -/
1257  lemma has_deriv_within_at.limsup_norm_slope_le
1258    (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) :
id           └─────────────────┘  └┘          └┘  
src          └─────────────────┘                    
typ          └─────────────────┘  └┘          └┘  
doc          └─────────────────┘
1259    ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
id     └┘  └┘ └─────────┘     └┘        
src    └┘   └┘ └─────────┘         └┘           
typ    └┘  └┘ └─────────┘     └┘        
doc    └┘   └┘ └─────────┘    
1260  begin
st   └─────
1261    have hr₀ : 0 < r, from lt_of_le_of_lt (norm_nonneg f') hr,
id                          └────────────┘  └─────────┘ └┘  └┘
src    └───────────┘   └───┘└────────────┘ └─────────┘  └┘
typ    └───────────┘  └───┘└────────────┘ └─────────┘└┘└┘└┘
doc    └───────────┘    └───┘                            └┘
txt    └───────────┘    └───┘                            └┘
par    └───────────┘    └───┘                            └┘
pid    └──────┘└───┘    └───┘                            └┘
st   ─────────────────┘└───────────────────────────────────────┘└─
1262    have A : ∀ᶠ z in nhds_within x (s \ {x}), ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
id              └┘   └┘ └─────────┘                └┘              └─┘ 
src    └───────┘└┘└─┘└┘└─────────┘   └─┘   └┘      └─┘
typ    └───────┘└┘└─┘└┘└─────────┘  └─┘   └┘     └─┘
doc    └───────┘└┘└─┘└┘└─────────┘     └─┘                └─┘
txt    └───────┘  └─┘                  └─┘                    
par    └───────┘  └─┘                  └─┘                    
pid    └────┘└─┘  └─┘                  └─┘                    
st   ────────────────────────────────────────────────────────────────────────────┘└─
1263      from (has_deriv_within_at_iff_tendsto_slope.1 hf).norm (mem_nhds_sets is_open_Iio hr),
id             └───────────────────────────────────┘   └┘        └───────────┘ └─────────┘ └┘
src      └───┘ └───────────────────────────────────┘└─┘  └─────┘ └───────────┘└─────────┘  
typ      └───┘ └───────────────────────────────────┘└─┘└┘└─────┘ └───────────┘└─────────┘└┘
doc      └───┘                                      └─┘  └─────┘                           
txt      └───┘                                      └─┘  └─────┘                           
par      └───┘                                      └─┘  └─────┘                           
pid      └───┘                                      └─┘  └─────┘                           
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
1264    have B : ∀ᶠ z in nhds_within x {x}, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
id              └┘   └┘ └─────────┘                                 └─┘ 
src    └───────┘└┘└─┘└┘└─────────┘ └┘                └─┘
typ    └───────┘└┘└─┘└┘└─────────┘ └┘               └─┘
doc    └───────┘└┘└─┘└┘└─────────┘  └┘                └─┘
txt    └───────┘  └─┘               └┘                    
par    └───────┘  └─┘               └┘                    
pid    └────┘└─┘  └─┘               └┘                    
st   ──────────────────────────────────────────────────────────────────────┘└─
1265      from mem_sets_of_superset self_mem_nhds_within
id            └──────────────────┘ └──────────────────┘
src      └───┘└──────────────────┘└──────────────────┘
typ      └───┘└──────────────────┘└──────────────────┘
doc      └───┘                                        
txt      └───┘                                        
par      └───┘                                        
pid      └───┘                                        
st   ───────────────────────────────────────────────────
1266        (singleton_subset_iff.2 $ by simp [hr₀]),
id          └──────────────────┘              └─┘
src  ─────┘ └──────────────────┘└─┘   └────┘   
typ  ─────┘ └──────────────────┘└─┘   └────┘└─┘
doc  ─────┘                     └─┘   └────┘   
txt  ─────┘                     └─┘   └────┘   
par  ─────┘                     └─┘   └────┘   
pid  ─────┘                     └─┘   └─────┘   └┘
st   ─────────────────────────────────┘└─────────┘└─
1267    have C := mem_sup_sets.2 ⟨A, B⟩,
id               └──────────┘      
src    └────────┘└──────────┘└─┘  └┘ 
typ    └────────┘└──────────┘└─┘ └┘
doc    └────────┘            └─┘  └┘ 
txt    └────────┘            └─┘  └┘ 
par    └────────┘            └─┘  └┘ 
pid    └────┘└─┘            └─┘  └┘ 
st   ────────────────────────────────┘└─
1268    rw [← nhds_within_union, diff_union_self, nhds_within_union, mem_sup_sets] at C,
id           └───────────────┘  └─────────────┘  └───────────────┘  └──────────┘
src    └────┘└───────────────┘└┘└─────────────┘└┘└───────────────┘└┘└──────────┘└────┘
typ    └────┘└───────────────┘└┘└─────────────┘└┘└───────────────┘└┘└──────────┘└────┘
doc    └────┘                 └┘               └┘                 └┘            └────┘
txt    └────┘                 └┘               └┘                 └┘            └────┘
par    └────┘                 └┘               └┘                 └┘            └────┘
pid      └──┘                 └┘               └┘                 └┘            └───┘
st   ────────────────────────┘└───────────────┘└─────────────────┘└────────────┘└───┘└─
1269    filter_upwards [C.1],
id                     
src    └──────────────┘ └─┘
typ    └──────────────┘└─┘
doc    └──────────────┘ └─┘
txt    └──────────────┘ └─┘
par    └──────────────┘ └─┘
pid                  └┘ └─┘
st   ─────────────────────┘└─
1270    simp only [mem_set_of_eq, norm_smul, mem_Iio, normed_field.norm_inv],
id                └───────────┘  └───────┘  └─────┘  └───────────────────┘
src    └─────────┘└───────────┘└┘└───────┘└┘└─────┘└┘└───────────────────┘
typ    └─────────┘└───────────┘└┘└───────┘└┘└─────┘└┘└───────────────────┘
doc    └─────────┘             └┘         └┘       └┘                     
txt    └─────────┘             └┘         └┘       └┘                     
par    └─────────┘             └┘         └┘       └┘                     
pid        └──┘└┘             └┘         └┘       └┘                     
st   ─────────────────────────────────────────────────────────────────────┘└─
1271    exact λ _, id
id                └┘
src    └────┘ └──┘└┘
typ    └────┘ └──┘└┘
doc    └────┘ └──┘  
txt    └────┘ └──┘  
par    └────┘ └──┘  
pid          └──┘  
st   ───────────────┘
1272  end
st   └─┘
1273  
1274  /-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ∥f'∥` the ratio
1275  `(∥f z∥ - ∥f x∥) / ∥z - x∥` is less than `r` in some neighborhood of `x` within `s`.
1276  In other words, the limit superior of this ratio as `z` tends to `x` along `s`
1277  is less than or equal to `∥f'∥`.
1278  
1279  This lemma is a weaker version of `has_deriv_within_at.limsup_norm_slope_le`
1280  where `∥f z∥ - ∥f x∥` is replaced by `∥f z - f x∥`. -/
1281  lemma has_deriv_within_at.limsup_slope_norm_le
1282    (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) :
id           └─────────────────┘  └┘          └┘  
src          └─────────────────┘                    
typ          └─────────────────┘  └┘          └┘  
doc          └─────────────────┘
1283    ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) < r :=
id     └┘  └┘ └─────────┘     └┘          
src    └┘   └┘ └─────────┘         └┘             
typ    └┘  └┘ └─────────┘     └┘          
doc    └┘   └┘ └─────────┘    
1284  begin
st   └─────
1285    apply (hf.limsup_norm_slope_le hr).mono,
id            └─────────────────────┘ └┘
src    └────┘ └─────────────────────┘  └────┘
typ    └────┘ └─────────────────────┘└┘└────┘
doc    └────┘ └─────────────────────┘  └────┘
txt    └────┘                          └────┘
par    └────┘                          └────┘
pid                                   └───┘
st   ────────────────────────────────────────┘└─
1286    assume z hz,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
1287    refine lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) _) hz,
id            └────────────┘  └───────────────────────┘  └──────────────┘         └┘
src    └─────┘└────────────┘ └───────────────────────┘ └──────────────┘└───────┘
typ    └─────┘└────────────┘ └───────────────────────┘ └──────────────┘└───────┘└┘
doc    └─────┘                                                         └───────┘
txt    └─────┘                                                         └───────┘
par    └─────┘                                                         └───────┘
pid                                                                   └───────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
1288    exact inv_nonneg.2 (norm_nonneg _)
id           └────────┘    └─────────┘
src    └────┘└────────┘└─┘ └─────────┘└──┘
typ    └────┘└────────┘└─┘ └─────────┘└──┘
doc    └────┘          └─┘            └──┘
txt    └────┘          └─┘            └──┘
par    └────┘          └─┘            └──┘
pid                   └─┘            └─┘
st   ────────────────────────────────────┘
1289  end
st   └─┘
1290  
1291  /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio
1292  `∥f z - f x∥ / ∥z - x∥` is frequently less than `r` as `z → x+0`.
1293  In other words, the limit inferior of this ratio as `z` tends to `x+0`
1294  is less than or equal to `∥f'∥`. See also `has_deriv_within_at.limsup_norm_slope_le`
1295  for a stronger version using limit superior and any set `s`. -/
1296  lemma has_deriv_within_at.liminf_right_norm_slope_le
1297    (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
id           └─────────────────┘  └┘  └─┘           └┘  
src          └─────────────────┘       └─┘                
typ          └─────────────────┘  └┘  └─┘           └┘  
doc          └─────────────────┘       └─┘
1298    ∃ᶠ z in nhds_within x (Ioi x), ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
id     └┘  └┘ └─────────┘   └─┘     └┘        
src    └┘   └┘ └─────────┘    └─┘        └┘           
typ    └┘  └┘ └─────────┘   └─┘     └┘        
doc    └┘   └┘ └─────────┘    └─┘   
1299  (hf.limsup_norm_slope_le hr).frequently (nhds_within_Ioi_self_ne_bot x)
id    └┘└───────────────────┘ └┘ └────────┘   └─────────────────────────┘ 
src     └───────────────────┘    └────────┘   └─────────────────────────┘
typ   └┘└───────────────────┘ └┘ └────────┘   └─────────────────────────┘ 
doc     └───────────────────┘
1300  
1301  /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio
1302  `(∥f z∥ - ∥f x∥) / (z - x)` is frequently less than `r` as `z → x+0`.
1303  In other words, the limit inferior of this ratio as `z` tends to `x+0`
1304  is less than or equal to `∥f'∥`.
1305  
1306  See also
1307  
1308  * `has_deriv_within_at.limsup_norm_slope_le` for a stronger version using
1309    limit superior and any set `s`;
1310  * `has_deriv_within_at.liminf_right_norm_slope_le` for a stronger version using
1311    `∥f z - f x∥` instead of `∥f z∥ - ∥f x∥`. -/
1312  lemma has_deriv_within_at.liminf_right_slope_norm_le
1313    (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
id           └─────────────────┘  └┘  └─┘           └┘  
src          └─────────────────┘       └─┘                
typ          └─────────────────┘  └┘  └─┘           └┘  
doc          └─────────────────┘       └─┘
1314    ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
id     └┘  └┘ └─────────┘   └─┘       └┘          
src    └┘   └┘ └─────────┘    └─┘          └┘             
typ    └┘  └┘ └─────────┘   └─┘       └┘          
doc    └┘   └┘ └─────────┘    └─┘   
1315  begin
st   └─────
1316    have := (hf.limsup_slope_norm_le hr).frequently (nhds_within_Ioi_self_ne_bot x),
id              └─────────────────────┘ └┘              └─────────────────────────┘ 
src    └──────┘ └─────────────────────┘  └───────────┘ └─────────────────────────┘ 
typ    └──────┘ └─────────────────────┘└┘└───────────┘ └─────────────────────────┘
doc    └──────┘ └─────────────────────┘  └───────────┘                             
txt    └──────┘                          └───────────┘                             
par    └──────┘                          └───────────┘                             
pid    └───┘└─┘                          └───────────┘                             
st   ────────────────────────────────────────────────────────────────────────────────┘└─
1317    refine this.mp (eventually.mono self_mem_nhds_within _),
id            └─────┘  └─────────────┘ └──────────────────┘
src    └─────┘└─────┘ └─────────────┘└──────────────────┘└─┘
typ    └─────┘└─────┘ └─────────────┘└──────────────────┘└─┘
doc    └─────┘                                           └─┘
txt    └─────┘                                           └─┘
par    └─────┘                                           └─┘
pid                                                     └─┘
st   ────────────────────────────────────────────────────────┘└─
1318    assume z hxz hz,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid    └─────────────┘
st   ────────────────┘└─
1319    rwa [real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz
id          └──────────────┘  └────────┘  └───────────┘ └─┘
src    └───┘└──────────────┘└┘└────────┘ └───────────┘   └───────┘
typ    └───┘└──────────────┘└┘└────────┘ └───────────┘└─┘└───────┘
doc    └───┘                └┘                           └───────┘
txt    └───┘                └┘                           └───────┘
par    └───┘                └┘                           └───────┘
pid       └┘                └┘                           └┘└────┘
st   ──────────────────────┘└──────────────────────────────┘└─────┘
1320  end
st   └─┘
1321  
1322  end real_space